small_iUnion — Mathlib

English

If each s(i) is small, then the union over i of s(i) is small.

Русский

Если каждый s(i) мал в α, то объединение ⋃ᵢ s(i) тоже малое.

LaTeX

$$$\bigl( \forall i, \operatorname{Small}(s(i)) \bigr) \Rightarrow \operatorname{Small}\Bigl(\bigcup_{i} s(i)\Bigr)$$$

Lean4

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

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