Results about Small on coerced sets

theorem small_subset {α : Type u1} {s : Set α} {t : Set α} (hts : t ⊆ s) [Small.{u, u1} ↑s] : Small.{u, u1} ↑t

instance small_powerset {α : Type u1} (s : Set α) [Small.{u, u1} ↑s] : Small.{u, u1} ↑(𝒫 s)

Equations

• ⋯ = ⋯

instance small_setProd {α : Type u1} {β : Type u2} (s : Set α) (t : Set β) [Small.{u, u1} ↑s] [Small.{u, u2} ↑t] : Small.{u, max u1 u2} ↑(s ×ˢ 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} α] : Small.{u, u2} ↑(Set.range f)

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] : Small.{u, u3} ↑(Set.image2 f s t)

Equations

• ⋯ = ⋯

theorem small_univ_iff {α : Type u1} : Small.{u, u1} ↑Set.univ ↔ Small.{u, 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] : Small.{u, u1} ↑(s ∪ 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] : Small.{u, u1} ↑(⋃₀ s)

Equations

• ⋯ = ⋯

instance small_biUnion {α : Type u1} {ι : Type u4} (s : Set ι) [Small.{u, u4} ↑s] (f : (i : ι) → i ∈ s → Set α) [∀ (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] : Small.{u, u1} ↑(insert x 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] : Small.{u, u1} ↑(s ∩ t)

Equations

• ⋯ = ⋯

instance small_inter_of_right {α : Type u1} (s : Set α) (t : Set α) [Small.{u, u1} ↑t] : Small.{u, u1} ↑(s ∩ 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] : Small.{u, u1} ↑(⋂₀ s)

instance small_sInter' {α : Type u1} {s : Set (Set α)} [Nonempty ↑s] [∀ (t : ↑s), Small.{u, u1} ↑↑t] : Small.{u, u1} ↑(⋂₀ s)

Equations

• ⋯ = ⋯

theorem small_biInter {α : Type u1} {ι : Type u4} {s : Set ι} {i : ι} (hi : i ∈ s) (f : (i : ι) → i ∈ s → Set α) [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 ∈ s → Set α) [∀ (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} : Small.{u, u1} ↑∅

theorem small_single {α : Type u1} (x : α) : Small.{u, u1} ↑{x}

theorem small_pair {α : Type u1} (x : α) (y : α) : Small.{u, u1} ↑{x, y}