coe_injective — Mathlib

English

The coercion from NNReal to Real is injective: equal real values imply equal NNReal numbers.

Русский

Вторая проекция из NNReal в Real является инъективной: равные действительные значения соответствуют равным NNReal.

LaTeX

$$$ \text{Injective}(\,\uparrow:\mathbb{R}_{\ge 0} \to \mathbb{R}\,) $$$

Lean4

protected theorem coe_injective : Injective ((↑) : ℝ≥0 → ℝ) :=
  Subtype.coe_injective

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