Theorem EMetric.exists_continuous_nnreal_forall_closedBall_subset

Modification history

2026-02-01 00:20
Mathlib/Topology/MetricSpace/PartitionOfUnity.lean
refactor(EMetricSpace): rename `EMetric.ball` -> `Metric.eball` (#34379) …
Deleted EMetric.exists_continuous_nnreal_forall_closedBall_subsetView on Github →
2024-02-09 13:35
Mathlib/Topology/MetricSpace/PartitionOfUnity.lean
chore: rename declarations containing `nNReal` to `nnreal` (#10372)
Added EMetric.exists_continuous_nnreal_forall_closedBall_subsetView on Github →