norm_sub_mul_le' — Mathlib

English

Let a, b, c be in a seminormed ring and suppose ∥b∥ ≤ 1. Then ∥c − a b∥ ≤ ∥1 − a∥ + ∥c − b∥.

Русский

Пусть a, b, c лежат в семинормированном кольце и предположим, что ∥b∥ ≤ 1. Тогда ∥c − a b∥ ≤ ∥1 − a∥ + ∥c − b∥.

LaTeX

$$$\|c - a b\| ≤ \|1 - a\| + \|c - b\| \quad\text{ if } \|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 norm_sub_mul_le' (hb : ‖b‖ ≤ 1) : ‖c - a * b‖ ≤ ‖1 - a‖ + ‖c - b‖ := by rw [add_comm];
  exact norm_sub_mul_le (α := αᵐᵒᵖ) hb

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