norm_toCompl

Mathlib.Analysis.Normed.Group.HomCompletion

URI: https://scilib.ai/kg/mathlib#NormedAddCommGroup.norm_toCompl

English

The norm is preserved by the completion embedding: ||toCompl x|| = ||x||.

Русский

Норма сохраняется под включением в завершение: ||toCompl x|| = ||x||.

LaTeX

$$$ \| toCompl(x) \| = \| x \|.$$$

Lean4

theorem norm_toCompl (x : G) : ‖toCompl x‖ = ‖x‖ :=
  Completion.norm_coe x

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru