toSeminormedCommGroup_norm_eq — Mathlib

English

Let α be a commutative group and F a GroupSeminormClass on α. For every f ∈ F and every x ∈ α, the norm of x in the seminormed group constructed from f equals f(x).

Русский

Пусть α — коммутативная группа и F — класс GroupSeminormClass на α. Тогда для каждого f и x верна та же равенство: норма x равна f(x).

LaTeX

$$$\|x\| = f(x)$$$

Lean4

@[to_additive]
theorem toSeminormedCommGroup_norm_eq [CommGroup α] [GroupSeminormClass F α ℝ] (f : F) (x : α) :
    @norm _ (GroupSeminormClass.toSeminormedCommGroup f).toNorm x = f x :=
  rfl

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