norm_toLp_single

Mathlib.Analysis.Normed.Lp.PiLp

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

English

The symmetric of the curry isometry corresponds to the uncurry of the function.

Русский

Обратное карри-изометрии соответствует развёртке функции.

LaTeX

$$$\text{(piLpCurry 𝕜 p α).symm f = toLp p (Sigma.uncurry (\lambda i j, f i j))}$$$

Lean4

@[simp]
theorem norm_toLp_single (i : ι) (b : β i) : ‖toLp p (Pi.single i b)‖ = ‖b‖ :=
  congr_arg ((↑) : ℝ≥0 → ℝ) <| nnnorm_toLp_single p β i b

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

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

Разделы

Аффилиация

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