ofReal_lt_ofReal_iff'

Mathlib.Data.ENNReal.Real

URI: https://scilib.ai/kg/mathlib#ENNReal.ofReal_lt_ofReal_iff'

English

For p,q ∈ ℝ, ENNReal.ofReal p < ENNReal.ofReal q iff p < q and 0 < q.

Русский

Для p,q ∈ ℝ, ENNReal.ofReal p < ENNReal.ofReal q эквивалентно p < q и 0 < q.

LaTeX

$$$$ \\forall p,q \\in \\mathbb{R},\\; ENNReal.ofReal(p) < ENNReal(q) \\iff p < q \\land 0 < q. $$$$

Lean4

theorem ofReal_lt_ofReal_iff' {p q : ℝ} : ENNReal.ofReal p < .ofReal q ↔ p < q ∧ 0 < q :=
  coe_lt_coe.trans Real.toNNReal_lt_toNNReal_iff'

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

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

Разделы

Аффилиация

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