coe_norm — Mathlib

English

For x in a subgroup s of a normed group E, the norm computed in s equals the norm in E: ‖x‖ = ‖(x:E)‖.

Русский

Для x ∈ подгруппы s нормa вычисленная в s равна норме в E: ‖x‖ = ‖(x:E)‖.

LaTeX

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

Lean4

/-- If `x` is an element of a subgroup `s` of a seminormed group `E`, its norm in `s` is equal to
its norm in `E`. -/
@[to_additive (attr := simp) /-- If `x` is an element of a subgroup `s` of a seminormed group `E`,
    its norm in `s` is equal to its norm in `E`. -/
    ]
theorem coe_norm (x : s) : ‖x‖ = ‖(x : E)‖ :=
  rfl

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