lsingle — Mathlib

English

If p ≥ 1, the map i ↦ single p i is an isometry (norm-preserving embedding) into the lp space.

Русский

Если p ≥ 1, отображение i ↦ single p i является изометрией в lp пространство.

LaTeX

$$$\text{Isometry}(\text{lp.single } p i).$$$

Lean4

/-- `single` as a `LinearMap`. -/
@[simps]
def lsingle (p) (i : α) : E i →ₗ[𝕜] lp E p where
  toFun := lp.single p i
  __ := singleAddMonoidHom p i
  map_smul' := lp.single_smul p i

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