isOpen_left_of_isOpen_union — Mathlib

English

If s and t are separated and s ∪ t is open, then s is open.

Русский

Если s и t разделены, и их объединение открыто, то s открыто.

LaTeX

$$$ \mathrm{SeparatedNhds}(s,t) \land \mathrm{IsOpen}(s\cup t) \Rightarrow \mathrm{IsOpen}(s) $$$

Lean4

theorem isOpen_left_of_isOpen_union (hst : SeparatedNhds s t) (hst' : IsOpen (s ∪ t)) : IsOpen s :=
  by
  obtain ⟨u, v, hu, hv, hsu, htv, huv⟩ := hst
  suffices s = (s ∪ t) ∩ u from this ▸ hst'.inter hu
  rw [union_inter_distrib_right, (huv.symm.mono_left htv).inter_eq, union_empty, inter_eq_left.2 hsu]

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