Mathlib.Logic.Small.Set

small_subset theorem

{s t : Set α} (hts : t ⊆ s) [Small.{u} s] : Small.{u} t

Full source

theorem small_subset {s t : Set α} (hts : t ⊆ s) [Small.{u} s] : Small.{u} t :=
  small_of_injective (Set.inclusion_injective hts)

Subset of Small Set is Small

Informal description

For any sets $s$ and $t$ in a type $\alpha$, if $t$ is a subset of $s$ (i.e., $t \subseteq s$) and $s$ is small (in universe level $u$), then $t$ is also small (in the same universe level $u$).

small_powerset instance

(s : Set α) [Small.{u} s] : Small.{u} (𝒫 s)

Full source

instance small_powerset (s : Set α) [Small.{u} s] : Small.{u} (𝒫 s) :=
  small_map (Equiv.Set.powerset s)

Smallness of Power Sets

Informal description

For any set $s$ in a type $\alpha$, if $s$ is small, then its power set $\mathcal{P}(s)$ is also small.

small_setProd instance

(s : Set α) (t : Set β) [Small.{u} s] [Small.{u} t] : Small.{u} (s ×ˢ t : Set (α × β))

Full source

instance small_setProd (s : Set α) (t : Set β) [Small.{u} s] [Small.{u} t] :
    Small.{u} (s ×ˢ t : Set (α × β)) :=
  small_of_injective (Equiv.Set.prod s t).injective

Smallness of Cartesian Products of Small Sets

Informal description

For any sets $s \subseteq \alpha$ and $t \subseteq \beta$, if both $s$ and $t$ are small (in universe level $u$), then their Cartesian product $s \times t$ is also small (in the same universe level $u$).

small_setPi instance

 {β : α → Type u2} (s : (a : α) → Set (β a)) [Small.{u} α] [∀ a, Small.{u} (s a)] : Small.{u} (Set.pi Set.univ s)

Full source

instance small_setPi {β : α → Type u2} (s : (a : α) → Set (β a))
    [Small.{u} α] [∀ a, Small.{u} (s a)] : Small.{u} (Set.pi Set.univ s) :=
  small_of_injective (Equiv.Set.univPi s).injective

Smallness of Product Sets of Small Families

Informal description

For any family of types $\beta : \alpha \to \text{Type}$ and any family of sets $s : (a : \alpha) \to \text{Set} (\beta a)$, if $\alpha$ is small and each set $s(a)$ is small, then the product set $\prod_{a \in \alpha} s(a)$ is also small.

small_range instance

(f : α → β) [Small.{u} α] : Small.{u} (Set.range f)

Full source

instance small_range (f : α → β) [Small.{u} α] :
    Small.{u} (Set.range f) :=
  small_of_surjective Set.surjective_onto_range

Smallness of the Range of a Function from a Small Type

Informal description

For any function $f : \alpha \to \beta$, if the type $\alpha$ is small, then the range of $f$ is also small.

small_image instance

(f : α → β) (s : Set α) [Small.{u} s] : Small.{u} (f '' s)

Full source

instance small_image (f : α → β) (s : Set α) [Small.{u} s] :
    Small.{u} (f '' s) :=
  small_of_surjective Set.surjective_onto_image

Images of Small Sets are Small

Informal description

For any function $f : \alpha \to \beta$ and any subset $s \subseteq \alpha$, if $s$ is small, then the image $f(s)$ is also small.

small_image2 instance

(f : α → β → γ) (s : Set α) (t : Set β) [Small.{u} s] [Small.{u} t] : Small.{u} (Set.image2 f s t)

Full source

instance small_image2 (f : α → β → γ) (s : Set α) (t : Set β) [Small.{u} s] [Small.{u} t] :
    Small.{u} (Set.image2 f s t) := by
  rw [← Set.image_uncurry_prod]
  infer_instance

Smallness of Images under Binary Functions on Small Sets

Informal description

For any function $f : \alpha \to \beta \to \gamma$ and sets $s \subseteq \alpha$, $t \subseteq \beta$, if both $s$ and $t$ are small (in universe level $u$), then the image $\{f(a, b) \mid a \in s, b \in t\}$ is also small (in universe level $u$).

small_univ_iff theorem

: Small.{u} (@Set.univ α) ↔ Small.{u} α

Full source

theorem small_univ_iff : SmallSmall.{u} (@Set.univ α) ↔ Small.{u} α :=
  small_congr <| Equiv.Set.univ α

Equivalence of Smallness Between Type and its Universal Set

Informal description

For any type $\alpha$, the universal set $\text{univ} \subseteq \alpha$ is small (in universe level $u$) if and only if the type $\alpha$ itself is small (in universe level $u$).

small_univ instance

[h : Small.{u} α] : Small.{u} (@Set.univ α)

Full source

instance small_univ [h : Small.{u} α] : Small.{u} (@Set.univ α) :=
  small_univ_iff.2 h

Smallness of the Universal Set for Small Types

Informal description

For any type $\alpha$ that is small (in universe level $u$), the universal set $\text{univ} \subseteq \alpha$ is also small (in universe level $u$).

small_union instance

(s t : Set α) [Small.{u} s] [Small.{u} t] : Small.{u} (s ∪ t : Set α)

Full source

instance small_union (s t : Set α) [Small.{u} s] [Small.{u} t] :
    Small.{u} (s ∪ t : Set α) := by
  rw [← Subtype.range_val (s := s), ← Subtype.range_val (s := t), ← Set.Sum.elim_range]
  infer_instance

Smallness of Union of Small Sets

Informal description

For any two sets $s$ and $t$ in a type $\alpha$, if both $s$ and $t$ are small, then their union $s \cup t$ is also small.

small_iUnion instance

[Small.{u} ι] (s : ι → Set α) [∀ i, Small.{u} (s i)] : Small.{u} (⋃ i, s i)

Full source

instance small_iUnion [Small.{u} ι] (s : ι → Set α)
    [∀ i, Small.{u} (s i)] : Small.{u} (⋃ i, s i) :=
  small_of_surjective <| Set.sigmaToiUnion_surjective _

Smallness of Union over a Small Index Type

Informal description

For any type $\iota$ that is `Small` (meaning it can be embedded into a universe of smaller cardinality) and any family of sets $s : \iota \to \text{Set } \alpha$ where each $s(i)$ is `Small`, the union $\bigcup_{i} s(i)$ is also `Small`.

small_sUnion instance

(s : Set (Set α)) [Small.{u} s] [∀ t : s, Small.{u} t] : Small.{u} (⋃₀ s)

Full source

instance small_sUnion (s : Set (Set α)) [Small.{u} s] [∀ t : s, Small.{u} t] :
    Small.{u} (⋃₀ s) :=
  Set.sUnion_eq_iUnion ▸ small_iUnion _

Smallness of Union over a Small Family of Sets

Informal description

For any family of sets $s$ of subsets of a type $\alpha$, if $s$ is `Small` and every subset $t$ in $s$ is `Small`, then the union $\bigcup_{t \in s} t$ is also `Small`.

small_biUnion instance

 (s : Set ι) [Small.{u} s] (f : (i : ι) → i ∈ s → Set α) [∀ i hi, Small.{u} (f i hi)] : Small.{u} (⋃ i, ⋃ hi, f i hi)

Full source

instance small_biUnion (s : Set ι) [Small.{u} s]
    (f : (i : ι) → i ∈ s → Set α) [∀ i hi, Small.{u} (f i hi)] : Small.{u} (⋃ i, ⋃ hi, f i hi) :=
  Set.biUnion_eq_iUnion s f ▸ small_iUnion _

Smallness of Bounded Union over a Small Index Set

Informal description

For any set $s$ of indices of type $\iota$ that is `Small` (meaning it can be embedded into a universe of smaller cardinality) and any family of sets $f$ indexed by $i \in s$ where each $f(i)$ is `Small`, the union $\bigcup_{i \in s} \bigcup_{h_i} f(i, h_i)$ is also `Small`.

small_insert instance

(x : α) (s : Set α) [Small.{u} s] : Small.{u} (insert x s : Set α)

Full source

instance small_insert (x : α) (s : Set α) [Small.{u} s] :
    Small.{u} (insert x s : Set α) :=
  Set.insert_eq x s ▸ small_union.{u} {x} s

Insertion of an Element Preserves Smallness of a Set

Informal description

For any element $x$ of type $\alpha$ and any set $s$ in $\alpha$, if $s$ is small, then the set $\{x\} \cup s$ is also small.

small_diff instance

(s t : Set α) [Small.{u} s] : Small.{u} (s \ t : Set α)

Full source

instance small_diff (s t : Set α) [Small.{u} s] : Small.{u} (s \ t : Set α) :=
  small_subset (Set.diff_subset)

Set Difference of Small Set is Small

Informal description

For any sets $s$ and $t$ in a type $\alpha$, if $s$ is small (in universe level $u$), then the set difference $s \setminus t$ is also small (in the same universe level $u$).

small_sep instance

(s : Set α) (P : α → Prop) [Small.{u} s] : Small.{u} {x | x ∈ s ∧ P x}

Full source

instance small_sep (s : Set α) (P : α → Prop) [Small.{u} s] :
    Small.{u} { x | x ∈ s ∧ P x} :=
  small_subset (Set.sep_subset s P)

Separation of a Small Set is Small

Informal description

For any set $s$ in a type $\alpha$ and any predicate $P$ on $\alpha$, if $s$ is small (in universe level $u$), then the subset $\{x \in s \mid P(x)\}$ is also small (in the same universe level $u$).

small_inter_of_left instance

(s t : Set α) [Small.{u} s] : Small.{u} (s ∩ t : Set α)

Full source

instance small_inter_of_left (s t : Set α) [Small.{u} s] :
    Small.{u} (s ∩ t : Set α) :=
  small_subset Set.inter_subset_left

Intersection with Small Set is Small (Left)

Informal description

For any sets $s$ and $t$ in a type $\alpha$, if $s$ is small (in universe level $u$), then the intersection $s \cap t$ is also small (in the same universe level $u$).

small_inter_of_right instance

(s t : Set α) [Small.{u} t] : Small.{u} (s ∩ t : Set α)

Full source

instance small_inter_of_right (s t : Set α) [Small.{u} t] :
    Small.{u} (s ∩ t : Set α) :=
  small_subset Set.inter_subset_right

Intersection with Small Set is Small (Right)

Informal description

For any sets $s$ and $t$ in a type $\alpha$, if $t$ is small (in universe level $u$), then the intersection $s \cap t$ is also small (in the same universe level $u$).

small_iInter theorem

(s : ι → Set α) (i : ι) [Small.{u} (s i)] : Small.{u} (⋂ i, s i)

Full source

theorem small_iInter (s : ι → Set α) (i : ι)
    [Small.{u} (s i)] : Small.{u} (⋂ i, s i) :=
  small_subset (Set.iInter_subset s i)

Intersection of Small Sets is Small

Informal description

For any family of sets $\{s_i\}_{i \in \iota}$ in a type $\alpha$ and any index $i \in \iota$, if the set $s_i$ is small (in universe level $u$), then the intersection $\bigcap_{i} s_i$ is also small (in the same universe level $u$).

small_iInter' instance

[Nonempty ι] (s : ι → Set α) [∀ i, Small.{u} (s i)] : Small.{u} (⋂ i, s i)

Full source

instance small_iInter' [Nonempty ι] (s : ι → Set α)
    [∀ i, Small.{u} (s i)] : Small.{u} (⋂ i, s i) :=
  let ⟨i⟩ : Nonempty ι := inferInstance
  small_iInter s i

Intersection of Small Sets is Small (Nonempty Case)

Informal description

For any nonempty index type $\iota$ and any family of sets $\{s_i\}_{i \in \iota}$ in a type $\alpha$, if each set $s_i$ is small (in universe level $u$), then the intersection $\bigcap_{i} s_i$ is also small (in the same universe level $u$).

small_sInter theorem

{s : Set (Set α)} {t : Set α} (ht : t ∈ s) [Small.{u} t] : Small.{u} (⋂₀ s)

Full source

theorem small_sInter {s : Set (Set α)} {t : Set α} (ht : t ∈ s)
    [Small.{u} t] : Small.{u} (⋂₀ s) :=
  Set.sInter_eq_iInter ▸ small_iInter _ ⟨t, ht⟩

Intersection of a Family of Sets is Small if a Member is Small

Informal description

For any family of sets $s$ in a type $\alpha$ and any set $t \in s$, if $t$ is small (in universe level $u$), then the intersection $\bigcap s$ is also small (in the same universe level $u$).

small_sInter' instance

{s : Set (Set α)} [Nonempty s] [∀ t : s, Small.{u} t] : Small.{u} (⋂₀ s)

Full source

instance small_sInter' {s : Set (Set α)} [Nonempty s]
    [∀ t : s, Small.{u} t] : Small.{u} (⋂₀ s) :=
  let ⟨t⟩ : Nonempty s := inferInstance
  small_sInter t.prop

Intersection of Small Sets is Small for Nonempty Family

Informal description

For any nonempty family of sets $s$ in a type $\alpha$, if every set $t \in s$ is small (in universe level $u$), then the intersection $\bigcap s$ is also small (in the same universe level $u$).

small_biInter theorem

 {s : Set ι} {i : ι} (hi : i ∈ s) (f : (i : ι) → i ∈ s → Set α) [Small.{u} (f i hi)] : Small.{u} (⋂ i, ⋂ hi, f i hi)

Full source

theorem small_biInter {s : Set ι} {i : ι} (hi : i ∈ s)
    (f : (i : ι) → i ∈ s → Set α) [Small.{u} (f i hi)] : Small.{u} (⋂ i, ⋂ hi, f i hi) :=
  Set.biInter_eq_iInter s f ▸ small_iInter _ ⟨i, hi⟩

Bounded Intersection of Small Sets is Small

Informal description

For any set $s$ of indices of type $\iota$, any index $i \in s$, and any family of sets $f$ indexed by $i \in s$ in a type $\alpha$, if the set $f(i)$ is small (in universe level $u$) for some $i \in s$, then the intersection $\bigcap_{i \in s} \bigcap_{h_i} f(i)$ is also small (in the same universe level $u$).

small_biInter' instance

 (s : Set ι) [Nonempty s] (f : (i : ι) → i ∈ s → Set α) [∀ i hi, Small.{u} (f i hi)] : Small.{u} (⋂ i, ⋂ hi, f i hi)

Full source

instance small_biInter' (s : Set ι) [Nonempty s]
    (f : (i : ι) → i ∈ s → Set α) [∀ i hi, Small.{u} (f i hi)] : Small.{u} (⋂ i, ⋂ hi, f i hi) :=
  let ⟨t⟩ : Nonempty s := inferInstance
  small_biInter t.prop f

Intersection of Small Sets is Small for Nonempty Index Set

Informal description

For any nonempty set $s$ of indices of type $\iota$ and any family of sets $f$ indexed by $i \in s$ in a type $\alpha$, if each set $f(i)$ is small (in universe level $u$), then the intersection $\bigcap_{i \in s} \bigcap_{h_i} f(i)$ is also small (in the same universe level $u$).

small_empty theorem

: Small.{u} (∅ : Set α)

Full source

theorem small_empty : Small.{u} (∅ : Set α) :=
  inferInstance

Empty Set is Small

Informal description

The empty set $\emptyset$ in a type $\alpha$ is small (with respect to universe level $u$).

small_single theorem

(x : α) : Small.{u} ({ x } : Set α)

Full source

theorem small_single (x : α) : Small.{u} ({x} : Set α) :=
  inferInstance

Singleton Sets are Small

Informal description

For any element $x$ of type $\alpha$, the singleton set $\{x\}$ is small.

small_pair theorem

(x y : α) : Small.{u} ({ x, y } : Set α)

Full source

theorem small_pair (x y : α) : Small.{u} ({x, y} : Set α) :=
  inferInstance

Pair Sets are Small

Informal description

For any elements $x$ and $y$ of type $\alpha$, the pair set $\{x, y\}$ is small (with respect to universe level $u$).