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
- ⋯ = ⋯
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
- ⋯ = ⋯