English
In a Hausdorff space X, for a compact t and x ∉ t, the set neighborhood filter of t and the neighborhood filter of x are disjoint: 𝓝ˢ t ⊓ 𝓝 x = ⊥.
Русский
В хаусдорфовом пространстве X для компактного t и точки x, не принадлежащей t, фильтры nhdsSet t и nhds x взаимно непересекаются.
LaTeX
$$$\forall X,[TopologicalSpace X],[T2Space X],\forall x\in X,\forall t\subseteq X\,\bigl(IsCompact t\land x\notin t\bigr)\Rightarrow Disjoint(𝓝ˢ t, 𝓝 x)$$$
Lean4
/-- In a `T2Space X`, for a compact set `t` and a point `x` outside `t`, `𝓝ˢ t` and `𝓝 x` are
disjoint. -/
theorem disjoint_nhdsSet_nhds {X : Type u_1} [TopologicalSpace X] [T2Space X] {x : X} {t : Set X} (H1 : IsCompact t)
(H2 : x ∉ t) : Disjoint (𝓝ˢ t) (𝓝 x) := by
simpa using
SeparatedNhds.disjoint_nhdsSet <|
.of_isCompact_isCompact_isClosed H1 isCompact_singleton isClosed_singleton <| disjoint_singleton_right.mpr H2
