toNorm

Mathlib.Analysis.Normed.Group.Constructions

URI: https://scilib.ai/kg/mathlib#Multiplicative.toNorm

English

The Norm on Multiplicative E agrees with the base norm: ∥x∥_{Multiplicative E} = ∥x∥_E.

Русский

Норма на Multiplicative E совпадает с исходной нормой: ∥x∥_{Multiplicative E} = ∥x∥_E.

LaTeX

$$$\|x\|_{\text{Multiplicative }E} = \|x\|_E$$$

Lean4

instance toNorm : Norm (Multiplicative E) :=
  ‹Norm E›

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru