Theorem EMetric.infEdist_prod

Modification history

2026-01-12 10:53

Mathlib/Topology/MetricSpace/HausdorffDistance.lean

chore(*): rename `EMetric.infEdist` -> `Metric.infEDist` etc (#33772) …

Deleted EMetric.infEdist_prod View on Github →

2025-11-05 12:23

Mathlib/Topology/MetricSpace/HausdorffDistance.lean

feat(Topology/MetricSpace/Closeds): Lipschitz continuity of product (#31223)

Added EMetric.infEdist_prod View on Github →