English
Let a, b, c lie in a seminormed ring and suppose ∥a∥ ≤ 1. Then ∥c − a b∥ ≤ ∥c − a∥ + ∥1 − b∥.
Русский
Пусть a, b, c лежат в семинормированном кольце и предположим, что ∥a∥ ≤ 1. Тогда ∥c − a b∥ ≤ ∥c − a∥ + ∥1 − b∥.
LaTeX
$$$\|c - a b\| ≤ \|c - a\| + \|1 - b\| \quad\text{ if } \|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 norm_sub_mul_le (ha : ‖a‖ ≤ 1) : ‖c - a * b‖ ≤ ‖c - a‖ + ‖1 - b‖ :=
calc
_ ≤ ‖c - a‖ + ‖a * (1 - b)‖ := by simpa [mul_one_sub] using norm_sub_le_norm_sub_add_norm_sub c a (a * b)
_ ≤ ‖c - a‖ + ‖a‖ * ‖1 - b‖ := by gcongr; exact norm_mul_le ..
_ ≤ ‖c - a‖ + 1 * ‖1 - b‖ := by gcongr
_ = ‖c - a‖ + ‖1 - b‖ := by simp
