countable_iUnion — Mathlib

English

If t(i) are countable for all i in a countable index set, then the union over i is countable.

Русский

Если $t(i)$ счетно для каждого i по счетному индексу, то объединение по i счетно.

LaTeX

$$$\\operatorname{Countable}(i) \\Rightarrow (\\bigcup_i t(i)) \\text{ Countable}$$$

Lean4

theorem countable_iUnion {t : ι → Set α} [Countable ι] (ht : ∀ i, (t i).Countable) : (⋃ i, t i).Countable :=
  by
  have := fun i ↦ (ht i).to_subtype
  rw [iUnion_eq_range_psigma]
  apply countable_range

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