toSeminormedGroup_norm_eq — Mathlib

English

Let α be a group and F a type of real-valued function on α equipped with a GroupSeminormClass structure. For every f ∈ F and every x ∈ α, the norm of x in the seminormed group associated to f is exactly f(x).

Русский

Пусть α — группа и F — множество отображений α → ℝ, снабжённое структурой GroupSeminormClass. Тогда для любого f ∈ F и любого x ∈ α норма x в семинормированной группе, ассоциированной с f, равна f(x).

LaTeX

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

Lean4

@[to_additive]
theorem toSeminormedGroup_norm_eq [Group α] [GroupSeminormClass F α ℝ] (f : F) (x : α) :
    @norm _ (GroupSeminormClass.toSeminormedGroup f).toNorm x = f x :=
  rfl

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