coe_sub — Mathlib

English

For r, p ∈ ℝ≥0, the ENNReal embedding preserves subtraction: (↑(r − p) : ℝ≥0∞) = ↑r − ↑p.

Русский

Пусть r, p ∈ ℝ≥0. Тогда сопряжение NNReal в ENNReal сохраняет вычитание: ↑(r − p) = ↑r − ↑p в ℝ≥0∞.

LaTeX

$$$$ (\uparrow (r - p) : \mathbb{R}_{\ge 0}^{\infty}) = \uparrow r - \uparrow p. $$$$

Lean4

/-- This is a special case of `WithTop.coe_sub` in the `ENNReal` namespace -/
@[simp, norm_cast]
theorem coe_sub : (↑(r - p) : ℝ≥0∞) = ↑r - ↑p :=
  WithTop.coe_sub

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