Theorem IsUltrametricDist.mem_closedBall_iff
Modification history
2025-08-17 08:01
Mathlib/Topology/MetricSpace/Ultra/Basic.lean
chore(Topology/MetricSpace/Ultra): deprecate `mem_ball_iff` and `mem_closedBall_iff` (duplicates) (#28524)
Deleted IsUltrametricDist.mem_closedBall_iffView on Github →