opNorm_zero_iff — Mathlib

English

In normed additive groups, the operator norm is zero if and only if the map is the zero map.

Русский

В нормированной аддитивной группе нормa оператора равна нулю тогда и только тогда, когда отображение ноль.

LaTeX

$$$$ \|f\| = 0 \iff f = 0 $$$$

Lean4

/-- For normed groups, an operator is zero iff its norm vanishes. -/
theorem opNorm_zero_iff {V₁ V₂ : Type*} [NormedAddCommGroup V₁] [NormedAddCommGroup V₂] {f : NormedAddGroupHom V₁ V₂} :
    ‖f‖ = 0 ↔ f = 0 :=
  Iff.intro
    (fun hn =>
      ext fun x =>
        norm_le_zero_iff.1
          (calc
            _ ≤ ‖f‖ * ‖x‖ := le_opNorm _ _
            _ = _ := by rw [hn, zero_mul]))
    fun hf => by rw [hf, opNorm_zero]

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