isSeparable_iUnion — Mathlib

English

For a countable index set, the union of separable sets is separable.

Русский

Для счётного индекса объединение сепарабельных множеств сепарабельно.

LaTeX

$$$\forall ι,[Countable\ ι],\forall s:ι\to Set(α), (\forall i, IsSeparable(s_i)) \Rightarrow IsSeparable(\bigcup_i s_i)$$$

Lean4

@[simp]
theorem isSeparable_iUnion {ι : Sort*} [Countable ι] {s : ι → Set α} :
    IsSeparable (⋃ i, s i) ↔ ∀ i, IsSeparable (s i) :=
  ⟨fun h i ↦ h.mono <| subset_iUnion s i, .iUnion⟩

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