singleContinuousLinearMap — Mathlib

English

For each i, the canonical embedding is a continuous linear map from E_i into lp(E,p).

Русский

Для каждого i каноническое вложение является непрерывным линейным отображением из E_i в lp(E,p).

LaTeX

$$$\\forall i, la_i \\in \\mathrm{ContLinearMap}(E_i, lp(E,p)).$$$

Lean4

/-- `lp.single` as a continuous linear map. -/
def singleContinuousLinearMap [Fact (1 ≤ p)] (i : α) : E i →L[𝕜] lp E p
    where
  __ := lsingle p i
  cont := isometry_single i |>.continuous

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