norm_incl — Mathlib

English

Let V be a normed additive group and V' ⊆ V an additive subgroup. The inclusion map incl: V' → V preserves the norm, i.e., ||incl(x)|| = ||x|| for all x ∈ V'.

Русский

Пусть V — нормированная аддитивная группа, V' ⊆ V — аддитивная подгруппа. Включение incl: V' → V сохраняет норму: ||incl(x)|| = ||x|| для всех x ∈ V'.

LaTeX

$$$\\|\\operatorname{incl}\\,x\\| = \\|x\\|$$$

Lean4

theorem norm_incl {V' : AddSubgroup V} (x : V') : ‖incl _ x‖ = ‖x‖ :=
  rfl

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