lpPiLp — Mathlib

English

There is a canonical equivalence between lp E p and PiLp p E whenever α is finite; the equivalence is given by viewing an lp element as a function, and vice versa.

Русский

Существует каноническое эквивалентное отображение между lp E p и PiLp p E при конечном α; эквивалентность переводит элемент lp в функцию и обратно.

LaTeX

$$$lp E p \simeq PiLp p E$$$

Lean4

/-- The canonical `Equiv` between `lp E p ≃ PiLp p E` when `E : α → Type u` with `[Finite α]`. -/
def lpPiLp : lp E p ≃ PiLp p E where
  toFun f := ⇑f
  invFun f := ⟨f, Memℓp.all f⟩

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