Theorems · Theorem · functional analysis

norm_sub_mul_le

∀ {α : Type u_2} [inst : SeminormedRing α] {a b c : α}, ‖a‖ ≤ 1 → ‖c - a * b‖ ≤ ‖c - a‖ + ‖1 - b‖

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.

Defined in

Mathlib.Analysis.Normed.Ring.Basic

Cited by

2 results in Mathlib

Foundations

Depth 113 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SeminormedRing