instNonUnitalSeminormedRing — Mathlib

English

In a suitable setting, the NN-norm of f equals the iSup of the pointwise NN-norms.

Русский

При соответствующих условиях NN-норма функции f равна iSup её точечных NN-норм.

LaTeX

$$$‖f‖_+ = iSup_{x} ‖f x‖_+$$$

Lean4

instance instNonUnitalSeminormedRing : NonUnitalSeminormedRing (α →ᵇ R)
    where
  __ := instSeminormedAddCommGroup
  __ := instNonUnitalRing
  norm_mul_le f
    g :=
    norm_ofNormedAddCommGroup_le _ (by positivity)
      (fun x ↦
        (norm_mul_le _ _).trans <|
          mul_le_mul (norm_coe_le_norm f x) (norm_coe_le_norm g x) (norm_nonneg _) (norm_nonneg _))

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