basisFun_repr — Mathlib

English

The basisFun basis for PiLp p β can be described as the Pi-basisFun mapped by the inverse of WithLp linear equivalence.

Русский

БазисBasis для PiLp p β совпадает с образом Pi.basisFun через обратное отображение линейного эквивалента WithLp.

LaTeX

$$$\mathrm{PiLp}.basisFun(p, \mathbb{𝕜}, ι) = (\mathrm{Pi.basisFun}(\mathbb{𝕜}, ι)).map(\mathrm{WithLp}.linearEquiv(p, \mathbb{𝕜}, (ι \to 𝕜))).symm$$$

Lean4

@[simp]
theorem basisFun_repr (x : PiLp p fun _ : ι => 𝕜) (i : ι) : (basisFun p 𝕜 ι).repr x i = x i :=
  rfl

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