toNNReal_lt_of_lt_coe

Mathlib.Data.ENNReal.Real

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

English

If a < p for some p ∈ NNReal, then a.toNNReal < p.

Русский

Если a < p для некоторого p ∈ NNReal, то a.toNNReal < p.

LaTeX

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

Lean4

theorem toNNReal_lt_of_lt_coe (h : a < p) : a.toNNReal < p :=
  @toNNReal_coe p ▸ toNNReal_strict_mono coe_ne_top h

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

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

Разделы

Аффилиация

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