opNorm_zero — Mathlib

English

The norm of the zero operator is zero: ||0|| = 0.

Русский

Норма нулевого оператора равна нулю: ||0|| = 0.

LaTeX

$$$$ \|0\| = 0 $$$$

Lean4

/-- The norm of the `0` operator is `0`. -/
theorem opNorm_zero : ‖(0 : NormedAddGroupHom V₁ V₂)‖ = 0 :=
  le_antisymm
    (csInf_le bounds_bddBelow
      ⟨ge_of_eq rfl, fun _ =>
        le_of_eq
          (by
            rw [zero_mul]
            exact norm_zero)⟩)
    (opNorm_nonneg _)

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