Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-02-22 22:26 bfa24650

View on Github →

refactor(topology/metric_space/lipschitz): redefine for an emetric_space (#2035)

refactor(topology/metric_space/lipschitz): redefine for an emetric_space
Fix compile
Fixes, thanks @sgouzel

Estimated changes

Modified src/analysis/ODE/gronwall.lean

Modified src/analysis/normed_space/finite_dimension.lean

Modified src/analysis/normed_space/operator_norm.lean

Modified src/data/real/ennreal.lean

added theorem ennreal.div_le_of_le_mul

added theorem ennreal.mul_lt_of_lt_div

Modified src/topology/bounded_continuous_function.lean

Modified src/topology/metric_space/closeds.lean

Modified src/topology/metric_space/contracting.lean

added theorem contracting_with.dist_le

modified def contracting_with

Modified src/topology/metric_space/gromov_hausdorff.lean

Modified src/topology/metric_space/gromov_hausdorff_realized.lean

Modified src/topology/metric_space/hausdorff_distance.lean

Modified src/topology/metric_space/lipschitz.lean

modified theorem lipschitz_with.diam_image_le

modified theorem lipschitz_with.ediam_image_le

added theorem lipschitz_with.edist_iterate_succ_le_geometric

added theorem lipschitz_with.edist_le

deleted theorem lipschitz_with.edist_map_le

added theorem lipschitz_with.nndist_le

deleted theorem lipschitz_with.nndist_map_le

modified def lipschitz_with

added theorem lipschitz_with_iff_dist_le