proj — Mathlib

English

For each i in ι, the i-th coordinate projection from PiLp p β to β_i is a continuous linear map.

Русский

Для каждого i из ι присутствует непрерывно-линейное отображение проекции на i-ю координату: PiLp p β →L[𝕜] β_i.

LaTeX

$$$\mathrm{proj}_i: \PiLp(p, \beta) \toL[\mathbb{𝕜}] \beta_i$$$

Lean4

/-- The projection on the `i`-th coordinate of `PiLp p β`, as a continuous linear map. -/
@[simps!]
def proj (i : ι) : PiLp p β →L[𝕜] β i where
  __ := projₗ p β i
  cont := continuous_apply ..

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