Theorem dist_mono_left

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_mono_leftView on Github →