Documentation

Mathlib.Topology.Category.LightProfinite.Sequence

The light profinite set classifying convergent sequences #

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

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

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

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

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