isClosed_right_of_isClosed_union — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem isClosed_right_of_isClosed_union (hst : SeparatedNhds s t) (hst' : IsClosed (s ∪ t)) : IsClosed t :=
  hst.symm.isClosed_left_of_isClosed_union (union_comm _ _ ▸ hst')

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