Theorem dist_le_dist_of_le

Modification history

2026-10-02 10:03
Mathlib/Analysis/Normed/Order/UpperLower.lean
feat(Analysis/Normed/Order): generalize distance lemmas to solid norms (#44072) …
Added dist_le_dist_of_leView on Github →