Theorems · Theorem · general topology

ClusterPt.exists_seq_tendsto

∀ {α : Type u} [t : TopologicalSpace α] [FirstCountableTopology α] {x : α} {f : Filter α} [f.IsCountablyGenerated],
  ClusterPt x f → ∃ ψ, Filter.Tendsto ψ Filter.atTop (nhds x) ∧ Filter.Tendsto ψ Filter.atTop f

In a first-countable space, a cluster point x of a countably generated filter is the limit of some sequence.

Defined in

Mathlib.Topology.Bases

Cited by

2 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceFirstCountableTopologyFilter.IsCountablyGenerated