le_toReal_sub — Mathlib

English

For ENNReal a,b with b ≠ ∞, we have a.toReal − b.toReal ≤ (a − b).toReal.

Русский

Для a,b ∈ ENNReal с b ≠ ∞ выполняется a.toReal − b.toReal ≤ (a − b).toReal.

LaTeX

$$$ b \neq \infty \Rightarrow a^{\text{toReal}} - b^{\text{toReal}} \le (a - b)^{\text{toReal}} $$$

Lean4

theorem le_toReal_sub {a b : ℝ≥0∞} (hb : b ≠ ∞) : a.toReal - b.toReal ≤ (a - b).toReal :=
  by
  lift b to ℝ≥0 using hb
  induction a
  · simp
  · simp only [← coe_sub, NNReal.sub_def, Real.coe_toNNReal', coe_toReal]
    exact le_max_left _ _

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