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 .

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.

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

@[deprecated LightProfinite.isClosedEmbedding_natUnionInftyEmbedding (since := "2024-10-20")]

Alias of LightProfinite.isClosedEmbedding_natUnionInftyEmbedding.


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

@[reducible, inline]

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

Equations

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

Equations