Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-02-26 22:16 0c1f285a

View on Github →

refactor(topology/metric_space): drop dist_setoid (#18502) Use uniform_space.separation_setoid instead.

Estimated changes

Modified src/topology/constructions.lean

added theorem continuous_sum_dom

Modified src/topology/metric_space/basic.lean

deleted def pseudo_metric.dist_setoid

deleted theorem pseudo_metric_quot_dist_eq

added theorem uniform_space.separation_quotient.dist_mk

Modified src/topology/metric_space/emetric_space.lean

added theorem uniform_space.separation_quotient.edist_mk

Modified src/topology/metric_space/gluing.lean

modified def metric.inductive_limit

modified def metric.to_glue_l

modified def metric.to_glue_r

Modified src/topology/metric_space/gromov_hausdorff.lean

modified def Gromov_Hausdorff.aux_gluing

Modified src/topology/metric_space/gromov_hausdorff_realized.lean

modified def Gromov_Hausdorff.optimal_GH_injl

modified def Gromov_Hausdorff.optimal_GH_injr

Modified src/topology/uniform_space/separation.lean

added theorem separation_rel_iff_inseparable

added theorem separation_rel_iff_specializes

added theorem uniform_space.separation_quotient.mk_eq_mk