English
For each index i, the canonical embedding x ↦ (with x at position i and zeros elsewhere) defines a continuous additive monoid hom from E_i into the lp-space; and, when p ≥ 1, this embedding is a continuous linear map.
Русский
Для каждого индекса i каноническое вложение x ↦ (x в i-ой позиции, нули в остальных) определяет непрерывное аддитивное однородное отображение из E_i в пространство lp; а при p ≥ 1 это вложение является непрерывным линейным отображением.
LaTeX
$$$\\forall i$, la_i: E_i \\to \\ell^p(E) \\text{ определено как } la_i(x) = (\\dots, 0, x, 0, \\dots) \\in \\ell^p(E),\\; la_i \\in \\mathrm{ContAddMonoidHom}(E_i,\\ell^p(E));\\text{ if } 1 \\le p\\text{ then } la_i \\in \\mathrm{ContLinearMap}(E_i,\\ell^p(E)).$$$
Lean4
/-- `lp.single` as a continuous morphism of additive monoids. -/
def singleContinuousAddMonoidHom [Fact (1 ≤ p)] (i : α) : ContinuousAddMonoidHom (E i) (lp E p)
where
__ := singleAddMonoidHom p i
continuous_toFun := isometry_single i |>.continuous
