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