basisFun_apply — Mathlib

English

The equivalence given by basisFun is equal to the WithLp linear equivalence between PiLp and the product space.

Русский

Эквиваленция, задаваемая basisFun, равна линейному эквиваленту WithLp между PiLp и произведением.

LaTeX

$$$\big(\text{basisFun}(p, \mathbb{𝕜}, ι)\big).equivFun = \mathrm{WithLp.lin earEq}(p, \mathbb{𝕜}, (ι \to 𝕜))$$$

Lean4

@[simp]
theorem basisFun_apply [DecidableEq ι] (i) : basisFun p 𝕜 ι i = toLp p (Pi.single i 1) := by
  simp_rw [basisFun, Basis.coe_ofEquivFun, WithLp.linearEquiv_symm_apply]

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