Theorem EMetric.dense_iff

Modification history

2026-02-01 00:20
Mathlib/Topology/EMetricSpace/Defs.lean
refactor(EMetricSpace): rename `EMetric.ball` -> `Metric.eball` (#34379) …
Modified EMetric.dense_iffView on Github →
2026-01-31 14:23
Mathlib/Topology/EMetricSpace/Defs.lean
feat: distance on the set of measurable sets given by the measure of the symmetric difference (#34517) …
Added EMetric.dense_iffView on Github →