nnnorm_coe — Mathlib

English

The nonnegative norm (nnnorm) on Completion E agrees with the original on embedded elements: ∥(x : Completion E)∥_{nn} = ∥x∥_{nn}.

Русский

Неотрицательная норма на Completion E совпадает с исходной нормой на встроенных элементах: ∥(x : Completion E)∥_{nn} = ∥x∥_{nn}.

LaTeX

$$$\|\,(x : Completion E)\|_{nn} = \|x\|_{nn}$$$

Lean4

@[simp]
theorem nnnorm_coe {E} [SeminormedAddCommGroup E] (x : E) : ‖(x : Completion E)‖₊ = ‖x‖₊ := by simp [nnnorm]

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