English
If s is compact and f: Y → X maps into s eventually along a filter l and y is the unique MapClusterPt of f along l in s, then f tends to nhds y along l.
Русский
Если s компактно и f: Y → X стремится в s по фильтру l, и y — единственный MapClusterPt для f вдоль l в s, то f стремится к nhds y вдоль l.
LaTeX
$$$IsCompact(s) \rightarrow (\forall f:\! Y \to X, \ \text{Eventually }(f(x) \in s)\ l) \rightarrow (\forall x \in s, MapClusterPt x l f \rightarrow x = y) \rightarrow Tendsto f l (𝓝 y)$$$
Lean4
/-- If values of `f : Y → X` belong to a compact set `s` eventually along a filter `l`
and `y` is a unique `MapClusterPt` for `f` along `l` in `s`,
then `f` tends to `𝓝 y` along `l`. -/
theorem tendsto_nhds_of_unique_mapClusterPt {Y} {l : Filter Y} {y : X} {f : Y → X} (hs : IsCompact s)
(hmem : ∀ᶠ x in l, f x ∈ s) (h : ∀ x ∈ s, MapClusterPt x l f → x = y) : Tendsto f l (𝓝 y) :=
hs.le_nhds_of_unique_clusterPt (mem_map.2 hmem) h
