toNNReal_eq_one

Mathlib.Data.NNReal.Defs

URI: https://scilib.ai/kg/mathlib#Real.toNNReal_eq_one

English

Real.toNNReal r = 1 iff r = 1.

Русский

Real.toNNReal r = 1 эквивалентно r = 1.

LaTeX

$$$$ r.toNNReal = 1 \\iff r = 1. $$$$

Lean4

@[simp]
theorem toNNReal_eq_one {r : ℝ} : r.toNNReal = 1 ↔ r = 1 :=
  toNNReal_eq_iff_eq_coe one_ne_zero

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

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

Разделы

Аффилиация

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