toReal_nonneg

Mathlib.Data.EReal.Basic

URI: https://scilib.ai/kg/mathlib#EReal.toReal_nonneg

English

Nonnegativity is preserved under toReal: if 0 ≤ x in EReal then 0 ≤ x.toReal.

Русский

Неотрицательность сохраняется: если 0 ≤ x в EReal, то 0 ≤ x.toReal.

LaTeX

$$$0 \le x \Rightarrow 0 \le x^{\mathrm{toReal}}$$$

Lean4

theorem toReal_nonneg {x : EReal} (hx : 0 ≤ x) : 0 ≤ x.toReal :=
  by
  cases x
  · simp
  · exact toReal_coe _ ▸ EReal.coe_nonneg.mp hx
  · simp

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

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

Разделы

Аффилиация

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