coe_lpPiLpₗᵢ

Mathlib.Analysis.Normed.Lp.LpEquiv

URI: https://scilib.ai/kg/mathlib#coe_lpPiLpₗᵢ

English

The symmetric version of the canonical lpPiLp is again a linear isometry between the same spaces.

Русский

Симметричная версия канонического lpPiLp снова линейная изометрия между теми же пространствами.

LaTeX

$$$lpPiLp_{\ell\!i} \text{ is a linear isometry }$$$

Lean4

theorem coe_lpPiLpₗᵢ [Fact (1 ≤ p)] (f : lp E p) : (lpPiLpₗᵢ E 𝕜 f : ∀ i, E i) = ⇑f :=
  rfl

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

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

Разделы

Аффилиация

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