English
In a Hausdorff space X, for a compact set t and a point x not in t, there exist open sets U and V separating t and x with t ⊆ U and x ∈ V and U ∩ V = ∅.
Русский
В хаусдорфовом пространстве X для компактного множества t и точки x, не принадлежащей t, существуют открытые множества U и V, разделяющие t и x, при этом t ⊆ U, x ∈ V и U ∩ V = ∅.
LaTeX
$$$\forall X,[TopologicalSpace X],[T2Space X],\forall t\subseteq X,\forall x\in X,IsCompact t\land x\notin t\Rightarrow \exists U,V\subseteq X\\IsOpen U\land IsOpen V\land t\subseteq U\land x\in V\land Disjoint U V$$$
Lean4
/-- In a `T2Space X`, for a compact set `t` and a point `x` outside `t`, there are open sets `U`,
`V` that separate `t` and `x`. -/
theorem separation_of_notMem {X : Type u_1} [TopologicalSpace X] [T2Space X] {x : X} {t : Set X} (H1 : IsCompact t)
(H2 : x ∉ t) : ∃ (U : Set X), ∃ (V : Set X), IsOpen U ∧ IsOpen V ∧ t ⊆ U ∧ x ∈ V ∧ Disjoint U V := by
simpa [SeparatedNhds] using
SeparatedNhds.of_isCompact_isCompact_isClosed H1 isCompact_singleton isClosed_singleton <|
disjoint_singleton_right.mpr H2
