English
In a Hausdorff space, if s and t are closed, and closure of s-complement is compact, and s and t are disjoint, then there exist neighborhoods that separate s and t.
Русский
В Хаусдорфовом пространстве, если s и t закрыты и замыкание комплемента s компактно, а s и t непересекаются, тогда существуют разделяющие окрестности.
LaTeX
$$$[T2Space X]\\; s,t\\subset X,\\; IsClosed s, IsClosed t,\\; IsCompact (closure (s^c))\\; \\Rightarrow \\ SeparatedNhds s t.$$$
Lean4
/-- In a `T2Space X`, for disjoint closed sets `s t` such that `closure sᶜ` is compact,
there are neighbourhoods that separate `s` and `t`. -/
theorem of_isClosed_isCompact_closure_compl_isClosed [T2Space X] {s : Set X} {t : Set X} (H1 : IsClosed s)
(H2 : IsCompact (closure sᶜ)) (H3 : IsClosed t) (H4 : Disjoint s t) : SeparatedNhds s t := by
-- Since `t` is a closed subset of the compact set `closure sᶜ`, it is compact.
have ht : IsCompact t := .of_isClosed_subset H2 H3 <| H4.subset_compl_left.trans subset_closure
rw [← diff_union_of_subset (interior_subset (s := s))]
-- since `t ⊆ sᶜ`, which is open, and `interior s` is open, we have
-- `SeparatedNhds (interior s) t`, which leaves us only with the frontier.
refine
.union_left ?_
⟨interior s, sᶜ, isOpen_interior, H1.isOpen_compl, le_rfl, H4.subset_compl_left,
disjoint_compl_right.mono_left interior_subset⟩
-- Since the frontier of `s` is compact (as it is a subset of `closure sᶜ`), we simply apply
-- `SeparatedNhds_of_isCompact_isCompact`.
rw [← H1.frontier_eq, frontier_eq_closure_inter_closure, H1.closure_eq]
refine .of_isCompact_isCompact ?_ ht (disjoint_of_subset_left inter_subset_left H4)
exact H2.of_isClosed_subset (H1.inter isClosed_closure) inter_subset_right
