prod_norm_toLp

Mathlib.Analysis.Normed.Lp.ProdLp

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

English

For f = (a,b), the Lp-norm of the ToLp image equals the norm of f in the product sense.

Русский

Для f = (a,b) норма Lp образа через toLp равна норме f в произведении.

LaTeX

$$$\|\mathrm{toLp}(\top, f)\| = \|f\|$$$

Lean4

@[simp]
theorem prod_norm_toLp (f : α × β) : ‖toLp ⊤ f‖ = ‖f‖ :=
  (prod_norm_ofLp _).symm

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

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

Разделы

Аффилиация

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