basisFun — Mathlib

English

There is a basis for the PiLp p β space indexed by ι, consisting of coordinate-like vectors; i.e., Basis ι 𝕜 (PiLp p (ι → 𝕜)).

Русский

Существует базис для пространства PiLp p(β) над 𝕜, индексированный множеством ι, состоящий из вектор-координат.

LaTeX

$$$\text{basisFun}: \mathsf{Basis}_{ι,\mathbb{𝕜}}(\PiLp(p, \beta))$$$

Lean4

/-- A version of `Pi.basisFun` for `PiLp`. -/
def basisFun : Basis ι 𝕜 (PiLp p fun _ : ι => 𝕜) :=
  Basis.ofEquivFun (WithLp.linearEquiv p 𝕜 (ι → 𝕜))

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