norm_coe — Mathlib

English

The norm on the completion preserves the original norm on embedded elements: for x in E, ∥(x : Completion E)∥ = ∥x∥.

Русский

Норма на завершении сохраняет норму исходного элемента: для x ∈ E, ∥(x в Completion E)∥ = ∥x∥.

LaTeX

$$$\|\,(x : Completion E)\| = \|x\|$$$

Lean4

@[simp]
theorem norm_coe {E} [SeminormedAddCommGroup E] (x : E) : ‖(x : Completion E)‖ = ‖x‖ :=
  Completion.extension_coe uniformContinuous_norm x

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