toNNReal_coe_nat

Mathlib.Data.NNReal.Defs

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

English

Real.toNNReal of a natural number equals the natural numeral in NNReal.

Русский

Real.toNNReal от натурального числа равняется числу-цифре в NNReal.

LaTeX

$$$ \\operatorname{Real.toNNReal}(n) = n \\quad \\text{for } n \\in \\mathbb{N}. $$$

Lean4

@[simp]
theorem _root_.Real.toNNReal_coe_nat (n : ℕ) : Real.toNNReal n = n :=
  NNReal.eq <| by simp [Real.coe_toNNReal]

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

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

Разделы

Аффилиация

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