isClosed_union_iff — Mathlib

English

SeparatedNhds s t implies IsClosed(s ∪ t) iff both s and t are closed.

Русский

Разделение Nhds s t эквивалентно замкнутости объединения, если обе части замкнуты.

LaTeX

$$$ \mathrm{IsClosed}(s\cup t) \iff (\mathrm{IsClosed}(s) \land \mathrm{IsClosed}(t)) $$$

Lean4

theorem isClosed_union_iff (hst : SeparatedNhds s t) : IsClosed (s ∪ t) ↔ IsClosed s ∧ IsClosed t :=
  ⟨fun h ↦ ⟨hst.isClosed_left_of_isClosed_union h, hst.isClosed_right_of_isClosed_union h⟩, fun ⟨h1, h2⟩ ↦ h1.union h2⟩

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