Commit 2025-11-05 12:23 c3f61400

View on Github →

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

Estimated changes

Modified Mathlib/Topology/MetricSpace/Closeds.lean

added theorem EMetric.NonemptyCompacts.lipschitz_prod

Modified Mathlib/Topology/MetricSpace/HausdorffDistance.lean

added theorem EMetric.hausdorffEdist_prod_le

added theorem EMetric.infEdist_prod