norm_incl_eq — Mathlib

English

The norm is preserved by inclusion into the completion: for all v, ||incl(v)|| = ||v||.

Русский

Норма сохраняется при включении в завершение: для всякого v выполняется ||incl(v)|| = ||v||.

LaTeX

$$$\\\\forall v \\\\in V:\\\\; \\\\|\\\\mathrm{completion.incl}(v)\\\\| = \\\\|v\\\\|.$$$

Lean4

theorem norm_incl_eq {V : SemiNormedGrp} {v : V} : ‖completion.incl v‖ = ‖v‖ :=
  UniformSpace.Completion.norm_coe _

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