tendsto_nhds_of_unique_mapClusterPt

English

If a map-cluster point for a function along a filter is unique, the function tends to that point.

Русский

Если для отображения вдоль фильтра существует уникальная карта кластерной точки, функция стремится к этой точке.

LaTeX

$$$\text{∀ x, MapClusterPt}(x,l,f) \Rightarrow \text{Tendsto } f\, l\ (\mathcal{N} y)\text{ для } y = x$$$

Lean4

/-- If `y` is a unique `MapClusterPt` for `f` along `l`
and the codomain of `f` is a compact space,
then `f` tends to `𝓝 y` along `l`. -/
theorem tendsto_nhds_of_unique_mapClusterPt [CompactSpace X] {Y} {l : Filter Y} {y : X} {f : Y → X}
    (h : ∀ x, MapClusterPt x l f → x = y) : Tendsto f l (𝓝 y) :=
  le_nhds_of_unique_clusterPt h

Похожие утверждения