toNNReal_one

Mathlib.Data.NNReal.Defs

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

English

Real.toNNReal 1 = 1.

Русский

Real.toNNReal 1 = 1.

LaTeX

$$$$ Real.toNNReal 1 = 1. $$$$

Lean4

@[simp]
theorem toNNReal_one : Real.toNNReal 1 = 1 :=
  NNReal.eq <| coe_toNNReal _ zero_le_one

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

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

Разделы

Аффилиация

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