The light profinite set classifying convergent sequences

This files defines the light profinite set ℕ∪{∞}, defined as the one point compactification of ℕ.

noncomputable def LightProfinite.natUnionInftyEmbedding : C(OnePoint ℕ, ℝ)

The continuous map from ℕ∪{∞} to ℝ sending n to 1/(n+1) and ∞ to 0.

Equations

• One or more equations did not get rendered due to their size.

theorem LightProfinite.closedEmbedding_natUnionInftyEmbedding : ClosedEmbedding ⇑LightProfinite.natUnionInftyEmbedding

The continuous map from ℕ∪{∞} to ℝ sending n to 1/(n+1) and ∞ to 0 is a closed embedding.

instance LightProfinite.instMetrizableSpaceOnePointNat : TopologicalSpace.MetrizableSpace (OnePoint ℕ)

Equations

• LightProfinite.instMetrizableSpaceOnePointNat = ⋯

@[reducible, inline]

abbrev LightProfinite.NatUnionInfty : LightProfinite

The one point compactification of the natural numbers as a light profinite set.

Equations

• LightProfinite.NatUnionInfty = LightProfinite.of (OnePoint ℕ)

def LightProfinite.«termℕ∪{∞}» : Lean.ParserDescr

The one point compactification of the natural numbers as a light profinite set.

Equations

• LightProfinite.«termℕ∪{∞}» = Lean.ParserDescr.node `LightProfinite.termℕ∪{∞} 1024 (Lean.ParserDescr.symbol "ℕ∪{∞}")

instance LightProfinite.instCoeNatαTopologicalSpaceToTopTrueToCompHausNatUnionInfty : Coe ℕ ↑LightProfinite.NatUnionInfty.toCompHaus.toTop

Equations

• LightProfinite.instCoeNatαTopologicalSpaceToTopTrueToCompHausNatUnionInfty = optionCoe

theorem LightProfinite.continuous_iff_convergent {Y : Type u_1} [TopologicalSpace Y] (f : ↑LightProfinite.NatUnionInfty.toCompHaus.toTop → Y) : Continuous f ↔ Filter.Tendsto (fun (x : ℕ) => f (some x)) Filter.atTop (nhds (f OnePoint.infty))