coe_lpPiLpₗᵢ_symm

Mathlib.Analysis.Normed.Lp.LpEquiv

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

English

If α is finite, every f: ∀ i, E_i lies in ℓ^p; i.e., Memℓp f p holds.

Русский

Если α конечно, то любой f: α → E_i принадлежит ℓ^p;

LaTeX

$$Memℓp f p$$

Lean4

theorem coe_lpPiLpₗᵢ_symm [Fact (1 ≤ p)] (f : PiLp p E) : ((lpPiLpₗᵢ E 𝕜).symm f : ∀ i, E i) = f :=
  rfl

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

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

Разделы

Аффилиация

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