The light profinite set classifying convergent sequences

This file 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.

theorem LightProfinite.isClosedEmbedding_natUnionInftyEmbedding : Topology.IsClosedEmbedding ⇑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 ℕ)

@[reducible, inline]

abbrev LightProfinite.NatUnionInfty : LightProfinite

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

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

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

@[implicit_reducible]

instance LightProfinite.instCoeNatCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopologyNatUnionInfty : Coe ℕ ↑NatUnionInfty.toTop

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