coe_comp_nnnorm' — Mathlib

English

The composition of real to NNReal norm equals the actual norm, i.e. (toReal ∘ nnNorm)(a) = ∥a∥.

Русский

Композиция вещественной конверсии и NNReal-нормы равна реальной норме: (toReal ∘ nnNorm)(a) = ∥a∥.

LaTeX

$$$\\big(\\mathrm{toReal} \\circ \\mathrm{nnnorm}\\big)(a) = \\|a\\|$$$

Lean4

@[to_additive (attr := simp) coe_comp_nnnorm]
theorem coe_comp_nnnorm' : (toReal : ℝ≥0 → ℝ) ∘ (nnnorm : E → ℝ≥0) = norm :=
  rfl

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