countable_iUnion_iff — Mathlib

English

For countable ι, (⋃ i, t(i)) is countable iff every t(i) is countable.

Русский

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

LaTeX

$$$\\operatorname{Countable}(\\mathbb{I}) \\Rightarrow (\\bigcup_i t(i)).Countable \\iff \\forall i, (t(i)).Countable$$$

Lean4

@[simp]
theorem countable_iUnion_iff [Countable ι] {t : ι → Set α} : (⋃ i, t i).Countable ↔ ∀ i, (t i).Countable :=
  ⟨fun h _ => h.mono <| subset_iUnion _ _, countable_iUnion⟩

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