Theorem EMetric.exists_forall_closedBall_subset_aux₁

Modification history

2023-05-17 06:40
Mathlib/Topology/MetricSpace/PartitionOfUnity.lean
feat: port Topology.MetricSpace.PartitionOfUnity (#3883)
Added EMetric.exists_forall_closedBall_subset_aux₁View on Github →