Commit 2023-05-17 06:40 f0287f32

View on Github →

feat: port Topology.MetricSpace.PartitionOfUnity (#3883)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/MetricSpace/PartitionOfUnity.lean

added theorem EMetric.eventually_nhds_zero_forall_closedBall_subset

added theorem EMetric.exists_continuous_eNNReal_forall_closedBall_subset

added theorem EMetric.exists_continuous_nNReal_forall_closedBall_subset

added theorem EMetric.exists_continuous_real_forall_closedBall_subset

added theorem EMetric.exists_forall_closedBall_subset_aux₁

added theorem EMetric.exists_forall_closedBall_subset_aux₂

added theorem Metric.exists_continuous_nNReal_forall_closedBall_subset

added theorem Metric.exists_continuous_real_forall_closedBall_subset