nnnorm_sub_mul_le' — Mathlib

English

If ∥b∥₊ ≤ 1, then ∥c − a b∥₊ ≤ ∥1 − a∥₊ + ∥c − b∥₊ in a seminormed ring.

Русский

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

LaTeX

$$$\|c - a b\|_{+} ≤ \|1 - a\|_{+} + \|c - b\|_{+} \quad\text{ when } \|b\|_{+} ≤ 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' (hb : ‖b‖₊ ≤ 1) : ‖c - a * b‖₊ ≤ ‖1 - a‖₊ + ‖c - b‖₊ :=
  norm_sub_mul_le' hb

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