Mathlib Changelog
v4
Changelog
About
Github
Theorem
Metric.exists_continuous_nNReal_forall_closedBall_subset
Modification history
2024-02-09 13:35
Mathlib/Topology/MetricSpace/PartitionOfUnity.lean
chore: rename declarations containing `nNReal` to `nnreal` (#10372)
Deleted
Metric.exists_continuous_nNReal_forall_closedBall_subset
View on Github →
2023-05-17 06:40
Mathlib/Topology/MetricSpace/PartitionOfUnity.lean
feat: port Topology.MetricSpace.PartitionOfUnity (#3883)
Added
Metric.exists_continuous_nNReal_forall_closedBall_subset
View on Github →