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

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.instCoeNatCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopologyNatUnionInfty : Coe ℕ ↑NatUnionInfty.toTop

Equations

• LightProfinite.instCoeNatCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopologyNatUnionInfty = optionCoe

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))