Documentation

Mathlib.Logic.Small.Set

Results about Small on coerced sets #

theorem small_subset {α : Type u1} {s : Set α} {t : Set α} (hts : t s) [Small.{u, u1} s] :
instance small_powerset {α : Type u1} (s : Set α) [Small.{u, u1} s] :
Equations
  • =
instance small_setProd {α : Type u1} {β : Type u2} (s : Set α) (t : Set β) [Small.{u, u1} s] [Small.{u, u2} t] :
Equations
  • =
instance small_setPi {α : Type u1} {β : αType u2} (s : (a : α) → Set (β a)) [Small.{u, u1} α] [∀ (a : α), Small.{u, u2} (s a)] :
Small.{u, max u1 u2} (Set.univ.pi s)
Equations
  • =
instance small_range {α : Type u1} {β : Type u2} (f : αβ) [Small.{u, u1} α] :
Equations
  • =
instance small_image {α : Type u1} {β : Type u2} (f : αβ) (s : Set α) [Small.{u, u1} s] :
Small.{u, u2} (f '' s)
Equations
  • =
instance small_image2 {α : Type u1} {β : Type u2} {γ : Type u3} (f : αβγ) (s : Set α) (t : Set β) [Small.{u, u1} s] [Small.{u, u2} t] :
Equations
  • =
theorem small_univ_iff {α : Type u1} :
instance small_univ {α : Type u1} [h : Small.{u, u1} α] :
Small.{u, u1} Set.univ
Equations
  • =
instance small_union {α : Type u1} (s : Set α) (t : Set α) [Small.{u, u1} s] [Small.{u, u1} t] :
Equations
  • =
instance small_iUnion {α : Type u1} {ι : Type u4} [Small.{u, u4} ι] (s : ιSet α) [∀ (i : ι), Small.{u, u1} (s i)] :
Small.{u, u1} (⋃ (i : ι), s i)
Equations
  • =
instance small_sUnion {α : Type u1} (s : Set (Set α)) [Small.{u, u1} s] [∀ (t : s), Small.{u, u1} t] :
Equations
  • =
instance small_biUnion {α : Type u1} {ι : Type u4} (s : Set ι) [Small.{u, u4} s] (f : (i : ι) → i sSet α) [∀ (i : ι) (hi : i s), Small.{u, u1} (f i hi)] :
Small.{u, u1} (⋃ (i : ι), ⋃ (hi : i s), f i hi)
Equations
  • =
instance small_insert {α : Type u1} (x : α) (s : Set α) [Small.{u, u1} s] :
Equations
  • =
instance small_diff {α : Type u1} (s : Set α) (t : Set α) [Small.{u, u1} s] :
Small.{u, u1} (s \ t)
Equations
  • =
instance small_sep {α : Type u1} (s : Set α) (P : αProp) [Small.{u, u1} s] :
Small.{u, u1} {x : α | x s P x}
Equations
  • =
instance small_inter_of_left {α : Type u1} (s : Set α) (t : Set α) [Small.{u, u1} s] :
Equations
  • =
instance small_inter_of_right {α : Type u1} (s : Set α) (t : Set α) [Small.{u, u1} t] :
Equations
  • =
theorem small_iInter {α : Type u1} {ι : Type u4} (s : ιSet α) (i : ι) [Small.{u, u1} (s i)] :
Small.{u, u1} (⋂ (i : ι), s i)
instance small_iInter' {α : Type u1} {ι : Type u4} [Nonempty ι] (s : ιSet α) [∀ (i : ι), Small.{u, u1} (s i)] :
Small.{u, u1} (⋂ (i : ι), s i)
Equations
  • =
theorem small_sInter {α : Type u1} {s : Set (Set α)} {t : Set α} (ht : t s) [Small.{u, u1} t] :
instance small_sInter' {α : Type u1} {s : Set (Set α)} [Nonempty s] [∀ (t : s), Small.{u, u1} t] :
Equations
  • =
theorem small_biInter {α : Type u1} {ι : Type u4} {s : Set ι} {i : ι} (hi : i s) (f : (i : ι) → i sSet α) [Small.{u, u1} (f i hi)] :
Small.{u, u1} (⋂ (i : ι), ⋂ (hi : i s), f i hi)
instance small_biInter' {α : Type u1} {ι : Type u4} (s : Set ι) [Nonempty s] (f : (i : ι) → i sSet α) [∀ (i : ι) (hi : i s), Small.{u, u1} (f i hi)] :
Small.{u, u1} (⋂ (i : ι), ⋂ (hi : i s), f i hi)
Equations
  • =
theorem small_empty {α : Type u1} :
theorem small_single {α : Type u1} (x : α) :
theorem small_pair {α : Type u1} (x : α) (y : α) :
Small.{u, u1} {x, y}