instHasSolidNorm — Mathlib

English

If, for all t, |f(t)| ≤ |g(t)| for bounded continuous functions f,g, then the norm of f is bounded by the norm of g in the natural Hadamard-like order: ||f|| ≤ ||g||.

Русский

Если для всех точек t выполняется |f(t)| ≤ |g(t)|, то норма f не превышает норму g.

LaTeX

$$$\forall f,g:\, \text{BoundedContinuousFunction}(f,g),\; (\forall t, \|f(t)\| ≤ \|g(t)\|) \Rightarrow \|f\| ≤ \|g\|.$$$

Lean4

instance instHasSolidNorm : HasSolidNorm (α →ᵇ β) :=
  {
    solid := by
      intro f g h
      have i1 : ∀ t, ‖f t‖ ≤ ‖g t‖ := fun t => HasSolidNorm.solid (h t)
      rw [norm_le (norm_nonneg _)]
      exact fun t => (i1 t).trans (norm_coe_le_norm g t) }

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