Commit 2023-04-17 07:01 cdb9a381

View on Github →

feat: port Topology.MetricSpace.Closeds (#3338)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/MetricSpace/Closeds.lean

added theorem EMetric.Closeds.edist_eq

added theorem EMetric.NonemptyCompacts.ToCloseds.uniformEmbedding

added theorem EMetric.NonemptyCompacts.isClosed_in_closeds

added theorem EMetric.continuous_infEdist_hausdorffEdist

added theorem EMetric.isClosed_subsets_of_isClosed

added theorem Metric.NonemptyCompacts.dist_eq

added theorem Metric.lipschitz_infDist

added theorem Metric.lipschitz_infDist_set

added theorem Metric.uniformContinuous_infDist_Hausdorff_dist