small_biUnion — Mathlib

English

The union over index i of the sets s(i) is small provided each s(i) is small.

Русский

Объединение по индексу i множеств s(i) мало при условии, что каждое s(i) мало.

LaTeX

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

Lean4

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 _

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