nnnorm_toLp

Mathlib.Analysis.Normed.Lp.PiLp

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

English

The norm of toLp ∞ f equals the norm of f: ‖toLp ∞ f‖ = ‖f‖.

Русский

Норма отображения toLp ∞ примененной к f равна норме f: ‖toLp ∞ f‖ = ‖f‖.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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