small_sUnion — Mathlib

English

The union ⋃₀ s of a small family s of sets is small if every member t ∈ s is small and s is small.

Русский

Объединение ⋃₀ s семейства малых множеств малое, если само множество s малое и каждый элемент t ∈ s мал.

LaTeX

$$$\operatorname{Small}(s) \land (\forall t \in s, \operatorname{Small}(t)) \Rightarrow \operatorname{Small}(\bigcup s)$$$

Lean4

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

Похожие утверждения