toReal_le_add' — Mathlib

English

If a ≤ b + c and notating conditions for ∞, then a.toReal ≤ b.toReal + c.toReal.

Русский

Если a ≤ b + c и выполнены условия для ∞, то a.toReal ≤ b.toReal + c.toReal.

LaTeX

$$toReal_le_add' hle hb hc$$

Lean4

/-- If `a ≤ b + c` and `a = ∞` whenever `b = ∞` or `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 = ∞ → a = ∞) (hc : c = ∞ → a = ∞) : a.toReal ≤ b.toReal + c.toReal :=
  by
  refine le_trans (toReal_mono' hle ?_) toReal_add_le
  simpa only [add_eq_top, or_imp] using And.intro hb hc

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