toReal_coe_nnnorm' — Mathlib

English

The nonnegative norm, viewed as a real number, equals the actual norm: (‖a‖₊ : ℝ≥0∞).toReal = ‖a‖.

Русский

Нон-негативная норма, приведенная к действительному числу, равна норме: (‖a‖₊ : ℝ≥0∞).toReal = ‖a‖.

LaTeX

$$$$ (\\|a\\|_{+} : \\mathbb{R}_{\\ge 0}^{\\infty}) .toReal = \\|a\\| $$$$

Lean4

/-- The nonnegative norm seen as an `ENNReal` and then as a `Real` is equal to the norm. -/
@[to_additive toReal_coe_nnnorm /-- The nonnegative norm seen as an `ENNReal` and
    then as a `Real` is equal to the norm. -/
    ]
theorem toReal_coe_nnnorm' (a : E) : (‖a‖₊ : ℝ≥0∞).toReal = ‖a‖ :=
  rfl

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