instCharZero — Mathlib

English

ENNReal has characteristic zero: the natural numbers embed injectively into ENNReal via n ↦ n copies of 1.

Русский

У ENNReal характеристика ноль: натуральные числа инъективно внедряются в ENNReal через n раз единицу.

LaTeX

$$$\mathbb{N} \\hookrightarrow \mathbb{R}_{\ge 0}^\infty \,\text{ via } n \mapsto \underbrace{1+\cdots+1}_{n \,\text{times}}$ is injective.$$

Lean4

instance : CharZero ℝ≥0∞ :=
  inferInstanceAs (CharZero (WithTop ℝ≥0))

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