Documentation

Mathlib.Topology.Category.LightProfinite.Sequence

The light profinite set classifying convergent sequences #

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

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

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

Instances For
    source
    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.

    source
    instance LightProfinite.instMetrizableSpaceOnePointNat :
    TopologicalSpace.MetrizableSpace (OnePoint ℕ)
    source
    @[reducible, inline]
    abbrev LightProfinite.NatUnionInfty :
    LightProfinite

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

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

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

      Instances For
        source
        @[implicit_reducible]
        instance LightProfinite.instCoeNatCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopologyNatUnionInfty :
        Coe ℕ ↑NatUnionInfty.toTop
        source
        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))