coe_nonpos

Mathlib.Data.EReal.Basic

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

English

Non-positivity is preserved: x ≤ 0 in EReal iff x ≤ 0 in Real.

Русский

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

LaTeX

$$$x \le 0 \ (\mathrm{in}\ EReal) \iff x \le 0 \ (\text{in Real})$$$

Lean4

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

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

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

Разделы

Аффилиация

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