coe_nonneg

Mathlib.Data.EReal.Basic

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

English

Nonnegativity is preserved: (0 ≤ x) in EReal iff 0 ≤ x in Real.

Русский

Ненегативность сохраняется: (0 ≤ x) в EReal эквивално 0 ≤ x в Real.

LaTeX

$$$\bigl(0:\!EReal\bigr) \le x \iff 0 \le x$$$

Lean4

@[simp, norm_cast]
protected theorem coe_nonneg {x : ℝ} : (0 : EReal) ≤ x ↔ 0 ≤ x :=
  EReal.coe_le_coe_iff

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

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

Разделы

Аффилиация

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