natUnionInftyEmbedding — Mathlib

English

The continuous map from OnePoint(N) to R sends ∞ to 0 and n to 1/(n+1).

Русский

Непрерывное отображение из OnePoint(N) в R отправляет ∞ в 0, а n в 1/(n+1).

LaTeX

$$$\mathrm{natUnionInftyEmbedding} : C(\mathrm{OnePoint}\,\mathbb{N}, \mathbb{R})$ with $\mathrm{toFun}(\infty)=0$, $\mathrm{toFun}(\mathrm{OnePoint.some} n)=\frac{1}{n+1}$, and continuous_toFun.$$

Lean4

/-- The continuous map from `ℕ∪{∞}` to `ℝ` sending `n` to `1/(n+1)` and `∞` to `0`. -/
noncomputable def natUnionInftyEmbedding : C(OnePoint ℕ, ℝ)
    where
  toFun
    | ∞ => 0
    | OnePoint.some n => 1 / (n + 1 : ℝ)
  continuous_toFun := OnePoint.continuous_iff_from_nat _ |>.mpr tendsto_one_div_add_atTop_nhds_zero_nat

Похожие утверждения