toReal_le_add — Mathlib

English

If a ≤ b + c and b, c are finite, then a.toReal ≤ b.toReal + c.toReal.

Русский

Если a ≤ b + c и b, c конечны, то a.toReal ≤ b.toReal + c.toReal.

LaTeX

$$toReal_le_add (hle := ?) (hb := ? ) (hc := ? )$$

Lean4

/-- If `a ≤ b + c`, `b ≠ ∞`, and `c ≠ ∞`, then
`ENNReal.toReal a ≤ ENNReal.toReal b + ENNReal.toReal c`. This lemma is useful to transfer
triangle-like inequalities from `ENNReal`s to `Real`s. -/
theorem toReal_le_add (hle : a ≤ b + c) (hb : b ≠ ∞) (hc : c ≠ ∞) : a.toReal ≤ b.toReal + c.toReal :=
  toReal_le_add' hle (flip absurd hb) (flip absurd hc)

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