toReal_add_le — Mathlib

English

(a + b).toReal ≤ a.toReal + b.toReal for ENNReal a,b.

Русский

(a + b).toReal ≤ a.toReal + b.toReal для ENNReal a,b.

LaTeX

$$$ (a + b).toReal \\le a.toReal + b.toReal $$$

Lean4

theorem toReal_add_le : (a + b).toReal ≤ a.toReal + b.toReal :=
  if ha : a = ∞ then by simp only [ha, top_add, toReal_top, zero_add, toReal_nonneg]
  else
    if hb : b = ∞ then by simp only [hb, add_top, toReal_top, add_zero, toReal_nonneg] else le_of_eq (toReal_add ha hb)

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