coe_add — Mathlib

English

Coercion commutes with addition: the real value of the sum equals the sum of the real values.

Русский

Коэрцирование сохраняет сложение: действительное значение суммы равно сумме действительных значений.

LaTeX

$$$ ((r_1 + r_2 : \mathbb{R}_{\ge 0}) : \mathbb{R}) = r_1 + r_2 $$$

Lean4

@[simp, norm_cast]
protected theorem coe_add (r₁ r₂ : ℝ≥0) : ((r₁ + r₂ : ℝ≥0) : ℝ) = r₁ + r₂ :=
  rfl

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