singleContinuousLinearMap_apply — Mathlib

English

For all i, the evaluation of the canonical linear map at i coincides with lp.single, i.e., the action on x ∈ E_i gives the same lp-element as lp.single p i x.

Русский

Для всех i применение канонического линейного отображения в i-ю координату совпадает с lp.single p i x.

LaTeX

$$$\\forall i,\\; singleContinuousLinearMap(p,i)(x) = lp.single(p,i)(x).$$$

Lean4

@[simp]
theorem singleContinuousLinearMap_apply [Fact (1 ≤ p)] (i : α) (x : E i) :
    singleContinuousLinearMap 𝕜 E p i x = lp.single p i x :=
  rfl

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