toNNReal_strict_mono

Mathlib.Data.ENNReal.Real

URI: https://scilib.ai/kg/mathlib#ENNReal.toNNReal_strict_mono

← MathLib Explorer

English

If b ≠ ∞ and a < b, then a.toNNReal < b.toNNReal.

Русский

Если b не ∞ и a < b, тогда a.toNNReal < b.toNNReal.

LaTeX

$$$$ \\forall a,b \\in \\mathbb{R}_{\\ge 0}^{\\infty},\\; b \\neq \\infty \\land a < b \\Rightarrow a^{\\mathrm{toNNReal}} < b^{\\mathrm{toNNReal}}. $$$$

Lean4

@[gcongr]
theorem toNNReal_strict_mono (hb : b ≠ ∞) (h : a < b) : a.toNNReal < b.toNNReal := by
  simpa [← ENNReal.coe_lt_coe, hb, h.ne_top]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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