norm_toLp_fst

Mathlib.Analysis.Normed.Lp.ProdLp

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

English

Let x ∈ α. The Lp-norm of (x, 0) equals the norm of x: ||toLp p (x,0)|| = ||x||.

Русский

Пусть x ∈ α. Норма Lp числа (x,0) равна норме x: ||toLp p (x,0)|| = ||x||.

LaTeX

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

Lean4

@[simp]
theorem norm_toLp_fst (x : α) : ‖toLp p (x, (0 : β))‖ = ‖x‖ :=
  congr_arg ((↑) : ℝ≥0 → ℝ) <| nnnorm_toLp_inl p α β x

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

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

Разделы

Аффилиация

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