coe_pos

Mathlib.Data.EReal.Basic

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

English

Strict positivity is preserved: (0 : EReal) < x ⇔ 0 < x.

Русский

Строгая положительность сохраняется: (0 : EReal) < x ⇔ 0 < x.

LaTeX

$$$\bigl(0: EReal\bigr) < x \iff 0 < x$$$

Lean4

@[simp, norm_cast]
protected theorem coe_pos {x : ℝ} : (0 : EReal) < x ↔ 0 < x :=
  EReal.coe_lt_coe_iff

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

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

Разделы

Аффилиация

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