isClosed_left_of_isClosed_union — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem isClosed_left_of_isClosed_union (hst : SeparatedNhds s t) (hst' : IsClosed (s ∪ t)) : IsClosed s :=
  by
  obtain ⟨u, v, hu, hv, hsu, htv, huv⟩ := hst
  rw [← isOpen_compl_iff] at hst' ⊢
  suffices sᶜ = (s ∪ t)ᶜ ∪ v from this ▸ hst'.union hv
  rw [← compl_inj_iff, Set.compl_union, compl_compl, compl_compl, union_inter_distrib_right,
    (disjoint_compl_right.mono_left htv).inter_eq, union_empty, left_eq_inter, subset_compl_comm]
  exact (huv.mono_left hsu).subset_compl_left

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