English
Let K be a compact subset of a R1-space X. Then y lies in the closure of K if and only if there exists x ∈ K with Inseparable x y.
Русский
Пусть K — компактное подмножество X, где X — R1-пространство. Тогда y принадлежит замыканию K тогда и только если существует x ∈ K такое, что Inseparable x y.
LaTeX
$$$ IsCompact K \\Rightarrow (y \\in \\overline{K} \\iff \\exists x \\in K, Inseparable x y). $$$
Lean4
/-- In an R₁ space, a point belongs to the closure of a compact set `K`
if and only if it is topologically inseparable from some point of `K`. -/
theorem mem_closure_iff_exists_inseparable {K : Set X} (hK : IsCompact K) : y ∈ closure K ↔ ∃ x ∈ K, Inseparable x y :=
by
refine ⟨fun hy ↦ ?_, fun ⟨x, hxK, hxy⟩ ↦ (hxy.mem_closed_iff isClosed_closure).1 <| subset_closure hxK⟩
contrapose! hy
have : Disjoint (𝓝 y) (𝓝ˢ K) :=
hK.disjoint_nhdsSet_right.2 fun x hx ↦ (disjoint_nhds_nhds_iff_not_inseparable.2 (hy x hx)).symm
simpa only [disjoint_iff, notMem_closure_iff_nhdsWithin_eq_bot] using this.mono_right principal_le_nhdsSet
