toNormedGroup_norm_eq — Mathlib

English

Let α be a group and F a GroupNormClass on α. For f ∈ F and x ∈ α, the norm in the NormedGroup obtained from f satisfies ∥x∥ = f(x).

Русский

Пусть α — группа и F — GroupNormClass на α. Тогда для любого f и x в α норма в полученной NormedGroup равна f(x).

LaTeX

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

Lean4

@[to_additive]
theorem toNormedGroup_norm_eq [Group α] [GroupNormClass F α ℝ] (f : F) (x : α) :
    @norm _ (GroupNormClass.toNormedGroup f).toNorm x = f x :=
  rfl

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