English
If s is compact and a filter l concentrates on s with a unique cluster point y in s, then l ≤ nhds y.
Русский
Если s компактно и l концентрируется на s, имея в s уникальную кластерную точку y, то l ⩽ nhds y.
LaTeX
$$$IsCompact(s) \rightarrow s \in l \rightarrow (\forall x \in s, ClusterPt x l \rightarrow x = y) \rightarrow l \le 𝓝 y$$$
Lean4
/-- If a compact set belongs to a filter and this filter has a unique cluster point `y` in this set,
then the filter is less than or equal to `𝓝 y`. -/
theorem le_nhds_of_unique_clusterPt (hs : IsCompact s) {l : Filter X} {y : X} (hmem : s ∈ l)
(h : ∀ x ∈ s, ClusterPt x l → x = y) : l ≤ 𝓝 y :=
by
refine le_iff_ultrafilter.2 fun f hf ↦ ?_
rcases hs.ultrafilter_le_nhds' f (hf hmem) with ⟨x, hxs, hx⟩
convert ← hx
exact h x hxs (.mono (.of_le_nhds hx) hf)
