Documentation

Mathlib.Logic.Small.Set

Results about Small on coerced sets #

theorem small_subset {α : Type v} {s : Set α} {t : Set α} (hts : t s) [Small.{u, v} s] :
instance small_range {α : Type v} {β : Type w} (f : αβ) [Small.{u, v} α] :
Equations
  • =
instance small_image {α : Type v} {β : Type w} (f : αβ) (S : Set α) [Small.{u, v} S] :
Small.{u, w} (f '' S)
Equations
  • =
instance small_union {α : Type v} (s : Set α) (t : Set α) [Small.{u, v} s] [Small.{u, v} t] :
Small.{u, v} (s t)
Equations
  • =
instance small_iUnion {α : Type v} {ι : Type w} [Small.{u, w} ι] (s : ιSet α) [∀ (i : ι), Small.{u, v} (s i)] :
Small.{u, v} (⋃ (i : ι), s i)
Equations
  • =
instance small_sUnion {α : Type v} (s : Set (Set α)) [Small.{u, v} s] [∀ (t : s), Small.{u, v} t] :
Equations
  • =