norm_ofLp

Mathlib.Analysis.Normed.Lp.PiLp

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

English

The norm of ofLp f equals the norm of f: ‖ofLp f‖ = ‖f‖.

Русский

Норма преобразования ofLp применяется к f сохраняется: ‖ofLp f‖ = ‖f‖.

LaTeX

$$$$ \|\mathrm{ofLp}\, f\| = \|f\| $$$$

Lean4

@[simp]
theorem norm_ofLp (f : PiLp ∞ β) : ‖ofLp f‖ = ‖f‖ :=
  congr_arg NNReal.toReal <| nnnorm_ofLp f

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

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

Разделы

Аффилиация

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