Theorem Metric.biInter_gt_ball

Modification history

2024-12-27 12:17
Mathlib/Topology/MetricSpace/Pseudo/Lemmas.lean
feat(MetricSpace): add `Metric.biInter_gt_ball` etc (#20262)
Added Metric.biInter_gt_ballView on Github →