coe_sub — Mathlib

English

If r2 ≤ r1, then the real value of (r1 − r2) in NNReal equals r1 − r2.

Русский

Если r2 ≤ r1, то действительное значение (r1 − r2) в NNReal равно r1 − r2.

LaTeX

$$$ (r_1 - r_2 : \mathbb{R}_{\ge 0}) : \mathbb{R} = r_1 - r_2 \quad \text{when } r_2 \le r_1 $$$

Lean4

@[simp, norm_cast]
protected theorem coe_sub {r₁ r₂ : ℝ≥0} (h : r₂ ≤ r₁) : ((r₁ - r₂ : ℝ≥0) : ℝ) = ↑r₁ - ↑r₂ :=
  max_eq_left <| le_sub_comm.2 <| by simp [show (r₂ : ℝ) ≤ r₁ from h]

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