norm_toLp_snd

Mathlib.Analysis.Normed.Lp.ProdLp

URI: https://scilib.ai/kg/mathlib#WithLp.norm_toLp_snd

English

Similarly, for y ∈ β, the Lp-norm of ((0), y) equals the norm of y: ||toLp p ((0, y))|| = ||y||.

Русский

Аналогично, для y ∈ β норма Lp числа ((0), y) равна норме y: ||toLp p ((0, y))|| = ||y||.

LaTeX

$$$\|toLp(p)((0,y))\| = \|y\|.$$$

Lean4

@[simp]
theorem norm_toLp_snd (y : β) : ‖toLp p ((0 : α), y)‖ = ‖y‖ :=
  congr_arg ((↑) : ℝ≥0 → ℝ) <| nnnorm_toLp_inr p α β y

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

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

Разделы

Аффилиация

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