nnnorm_sub_mul_le — Mathlib

English

In a seminormed ring, if ∥a∥∞ ≤ 1, then the nonnegative norm satisfies ∥c − a b∥₊ ≤ ∥c − a∥₊ + ∥1 − b∥₊.

Русский

В семинормированном кольце, если ∥a∥∞ ≤ 1, то неотрицательная нормa удовлетворяет ∥c − a b∥₊ ≤ ∥c − a∥₊ + ∥1 − b∥₊.

LaTeX

$$$\|c - a b\|_{+} ≤ \|c - a\|_{+} + \|1 - b\|_{+} \quad\text{ when } \|a\|_{+} ≤ 1$$$

Lean4

/-- This inequality is particularly useful when `c = 1` and `‖a‖ = ‖b‖ = 1` as it then shows that
chord length is a metric on the unit complex numbers. -/
theorem nnnorm_sub_mul_le (ha : ‖a‖₊ ≤ 1) : ‖c - a * b‖₊ ≤ ‖c - a‖₊ + ‖1 - b‖₊ :=
  norm_sub_mul_le ha

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