projₗ — Mathlib

English

The projection onto the i-th coordinate is a linear map from PiLp p β to β_i.

Русский

Проекция на i-ю координату является линейным отображением PiLp p β → β_i.

LaTeX

$$$\\mathrm{proj}_i: \\PiLp(p, \\beta) \\to_{} \\beta_i \\quad\\text{is linear}$$$

Lean4

/-- The projection on the `i`-th coordinate of `WithLp p (∀ i, α i)`, as a linear map. -/
@[simps!]
def projₗ (i : ι) : PiLp p β →ₗ[𝕜] β i :=
  (LinearMap.proj i : (∀ i, β i) →ₗ[𝕜] β i) ∘ₗ (WithLp.linearEquiv p 𝕜 (∀ i, β i)).toLinearMap

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