Commit 2024-09-02 07:30 00df099f
View on Github →feat: ‖c - a * b‖ ≤ ‖c - a‖ + ‖1 - b‖
when ‖a‖ ≤ 1
(#16318)
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 circle.
From LeanAPAP