norm_toLp

Mathlib.Analysis.Normed.Lp.PiLp

URI: https://scilib.ai/kg/mathlib#PiLp.norm_toLp

English

The norm of toLp ∞ f equals the NN-norm of f when considered by norm statements: the stated identity.

Русский

Норма toLp ∞ f равна NN-норме f в рамках соответствующих равенств.

LaTeX

$$$$ \|\mathrm{toLp}\,\infty\, f\| = \|f\|_+ $$$$

Lean4

@[simp]
theorem norm_toLp (f : ∀ i, β i) : ‖toLp ∞ f‖ = ‖f‖ :=
  (norm_ofLp _).symm

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

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

Разделы

Аффилиация

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