Commit 2025-11-06 20:50 de8851a2

View on Github →

feat(Topology/MetricSpace/Closeds): Lipschitz continuity of union (#30823)

Estimated changes

Modified Mathlib/Topology/MetricSpace/Closeds.lean

added theorem EMetric.Closeds.lipschitz_sup

added theorem EMetric.NonemptyCompacts.lipschitz_sup

Modified Mathlib/Topology/MetricSpace/HausdorffDistance.lean

added theorem EMetric.hausdorffEdist_iUnion_le

added theorem EMetric.hausdorffEdist_union_le