theorem
small_subset
{α : Type v}
{s : Set α}
{t : Set α}
(hts : t ⊆ s)
[Small.{u, v} ↑s]
:
Small.{u, v} ↑t
instance
small_range
{α : Type v}
{β : Type w}
(f : α → β)
[Small.{u, v} α]
:
Small.{u, w} ↑(Set.range f)
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]
:
Small.{u, v} ↑s.sUnion
Equations
- ⋯ = ⋯