Mathlib Changelog
v4
Changelog
About
Github
Theorem
tendsto_closedBall_smallSets
Modification history
2024-06-23 22:42
Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
chore(Topology/MetricSpace/PseudoMetric): Split (#13977) …
Modified
tendsto_closedBall_smallSets
View on Github →
2024-03-13 17:36
Mathlib/Topology/MetricSpace/PseudoMetric.lean
feat(MetricSpace): add `tendsto_closedBall_smallSets` (#11068) …
Added
tendsto_closedBall_smallSets
View on Github →