seminorm — Mathlib

English

If ∥m∥ ≤ 1, then ∥f m∥ ≤ ∥f∥.

Русский

Если ∥m∥ ≤ 1, то ∥f m∥ ≤ ∥f∥.

LaTeX

$$$$ \\|f m\\| ≤ \\|f\\| \\quad\\text{when}\\quad \\|m\\| ≤ 1.$$$$

Lean4

/-- Operator seminorm on the space of continuous multilinear maps, as `Seminorm`.

We use this seminorm
to define a `SeminormedAddCommGroup` structure on `ContinuousMultilinearMap 𝕜 E G`,
but we have to override the projection `UniformSpace`
so that it is definitionally equal to the one coming from the topologies on `E` and `G`. -/
protected def seminorm : Seminorm 𝕜 (ContinuousMultilinearMap 𝕜 E G) :=
  .ofSMulLE norm opNorm_zero opNorm_add_le fun c f ↦ f.opNorm_smul_le c

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