isOpen_union_iff — Mathlib

English

Separation from a pair is equivalent to both parts being open when the union is open.

Русский

Разделение пары эквивалентно тому, что обе части открыты при открытом их объединении.

LaTeX

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

Lean4

theorem isOpen_union_iff (hst : SeparatedNhds s t) : IsOpen (s ∪ t) ↔ IsOpen s ∧ IsOpen t :=
  ⟨fun h ↦ ⟨hst.isOpen_left_of_isOpen_union h, hst.isOpen_right_of_isOpen_union h⟩, fun ⟨h1, h2⟩ ↦ h1.union h2⟩

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