sUnion_iff — Mathlib

English

If s is countable, then the sUnion of s (i.e., union of sets in s) is countable iff every member a ∈ s is countable.

Русский

Если s счетно, то sUnion множества в s счетно тогда и только тогда, когда каждый элемент a ∈ s счетен.

LaTeX

$$$\\operatorname{Countable}(s) \\Rightarrow (\\bigcup s).Countable \\iff \\forall a \\in s, a.Countable$$$

Lean4

theorem sUnion_iff {s : Set (Set α)} (hs : s.Countable) : (⋃₀ s).Countable ↔ ∀ a ∈ s, a.Countable := by
  rw [sUnion_eq_biUnion, hs.biUnion_iff]

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