Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-03-19 22:37
db0c38c2
View on Github →
feat(EMetric):
closedBall x 0 = {x}
(
#23106
) From my PhD (MiscYD)
Estimated changes
Modified
Mathlib/Topology/EMetricSpace/Defs.lean
added
theorem
EMetric.closedBall_zero