Theorem Metric.biUnion_lt_closedBall

Modification history

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