coe_inj

Mathlib.Data.NNReal.Defs

URI: https://scilib.ai/kg/mathlib#NNReal.coe_inj

English

For NNReal numbers r1 and r2, (r1 : ℝ) = (r2) iff r1 = r2.

Русский

Для NNReal чисел r1 и r2 верно: (r1) = (r2) тогда и только тогда, когда r1 = r2.

LaTeX

$$$ (r_1 : \mathbb{R}) = r_2 \;\iff\; r_1 = r_2 $$$

Lean4

@[simp, norm_cast]
theorem coe_inj {r₁ r₂ : ℝ≥0} : (r₁ : ℝ) = r₂ ↔ r₁ = r₂ :=
  NNReal.coe_injective.eq_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru