Sequences of real numbers

• Convergence

DefinitionLimit point#

A point x is a cluster point of a sequence u along a filter F if it is a cluster point of map u F.

MapClusterPt.{u_1, u_3} {X : Type u_1} [TopologicalSpace X] {ι : Type u_3} (x : X) (F : Filter ι)
  (u : ι → X) : Prop

Sources

• Mathlib documentation: MapClusterPt
• Source of MapClusterPt in Mathlib/Topology/Defs/Filter.lean
• Mathlib undergraduate list: Single Variable Real Analysis › Sequences of real numbers

MathlibMapClusterPt

Uses 1 · Used by 1

Statement usesCluster point

Used bySequential compactness is equivalent to compactness (Bolzano-Weierstrass)

• Recurrent sequences
• Limit infimum and supremum
• Cauchy sequences

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.