basisFun_equivFun — Mathlib

English

The map equality relating PiLp basisFun and Pi basisFun commutes with the linear equivalence, producing equality of bases.

Русский

Соотношение отображения базиса PiLp и базиса Pi сохраняется под линейным эквивалентом, образуя равенство базисов.

LaTeX

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

Lean4

@[simp]
theorem basisFun_equivFun : (basisFun p 𝕜 ι).equivFun = WithLp.linearEquiv p 𝕜 (ι → 𝕜) :=
  Basis.equivFun_ofEquivFun _

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