toNNReal_of_nonpos

Mathlib.Data.NNReal.Defs

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

English

If r ≤ 0 then Real.toNNReal r = 0.

Русский

Если r ≤ 0, то Real.toNNReal r = 0.

LaTeX

$$$$ r \\le 0 \\;\\Rightarrow\\; Real.toNNReal r = 0. $$$$

Lean4

theorem toNNReal_of_nonpos {r : ℝ} : r ≤ 0 → Real.toNNReal r = 0 :=
  toNNReal_eq_zero.2

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

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

Разделы

Аффилиация

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