le_toNNReal_of_coe_le — Mathlib

English

If a ∈ ENNReal and p ∈ NNReal satisfy p ≤ a and a ≠ ∞, then p ≤ a.toNNReal.

Русский

Пусть a ∈ ENNReal и p ∈ NNReal satisfy p ≤ a и a ≠ ∞, тогда p ≤ a.toNNReal.

LaTeX

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

Lean4

theorem le_toNNReal_of_coe_le (h : p ≤ a) (ha : a ≠ ∞) : p ≤ a.toNNReal :=
  @toNNReal_coe p ▸ toNNReal_mono ha h

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