Theorems · Theorem · general topology

IsCompact.tendsto_nhds_of_unique_mapClusterPt

∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {Y : Type u_2} {l : Filter Y} {y : X} {f : Y → X},
  IsCompact s → (∀ᶠ (x : Y) in l, f x ∈ s) → (∀ x ∈ s, MapClusterPt x l f → x = y) → Filter.Tendsto f l (nhds y)

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.

Defined in

Mathlib.Topology.Compactness.Compact

Cited by

0 results in Mathlib

Foundations

Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpace