Theorem dist_anti_right_pi

Modification history

2026-10-02 10:03
Mathlib/Analysis/Normed/Order/UpperLower.lean
feat(Analysis/Normed/Order): generalize distance lemmas to solid norms (#44072) …
Deleted dist_anti_right_piView on Github →
2024-06-07 23:31
Mathlib/Analysis/Normed/Order/UpperLower.lean
feat: Topological properties of order-connected sets in ℝⁿ (#10565) …
Added dist_anti_right_piView on Github →