Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-20 17:12 f34bb6b9

View on Github →

refactor(topology/metric_space/lipschitz): review API of lipschitz_with (#1700)

refactor(topology/metric_space/lipschitz): review API of lipschitz_with
Take K : ℝ≥0 instead of using a conjuction;
Rename each *_of_lipschitz to lipschitz_with.*;
Define convenience constructors (e.g., of_le_add);
Move facts about contracting maps to a separate file&namespace;
Adjust other files to API changes.
Make the first argument of lipschitz_with.weaken implicit Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
Fix compile
Fix 'unused args' bug reported by #lint

Estimated changes

Modified src/analysis/normed_space/finite_dimension.lean

Modified src/analysis/normed_space/operator_norm.lean

modified theorem continuous_linear_map.lipschitz

added theorem linear_map.lipschitz_of_bound

added theorem linear_map.uniform_continuous_of_bound

Modified src/topology/bounded_continuous_function.lean

modified def bounded_continuous_function.comp

modified theorem bounded_continuous_function.continuous_comp

added theorem bounded_continuous_function.lipschitz_comp

added theorem bounded_continuous_function.uniform_continuous_comp

Modified src/topology/metric_space/closeds.lean

added theorem metric.lipschitz_inf_dist

added theorem metric.lipschitz_inf_dist_set

Created src/topology/metric_space/contracting.lean

added theorem contracting_with.aposteriori_dist_iterate_fixed_point_le

added theorem contracting_with.apriori_dist_iterate_fixed_point_le

added theorem contracting_with.dist_fixed_point_fixed_point_of_dist_le'

added theorem contracting_with.dist_fixed_point_le

added theorem contracting_with.dist_inequality

added theorem contracting_with.dist_le_of_fixed_point

added theorem contracting_with.exists_fixed_point

added theorem contracting_with.fixed_point_is_fixed

added theorem contracting_with.fixed_point_lipschitz_in_map

added theorem contracting_with.fixed_point_unique'

added theorem contracting_with.fixed_point_unique

added theorem contracting_with.one_sub_K_pos

added theorem contracting_with.to_lipschitz_with

added def contracting_with

added theorem fixed_point_of_tendsto_iterate

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

deleted theorem metric.continuous_inf_dist

added theorem metric.continuous_inf_dist_pt

added theorem metric.lipschitz_inf_dist_pt

deleted theorem metric.uniform_continuous_inf_dist

added theorem metric.uniform_continuous_inf_dist_pt

Modified src/topology/metric_space/lipschitz.lean

deleted theorem continuous_of_lipschitz

deleted theorem fixed_point_of_tendsto_iterate

added theorem lipschitz_with.diam_image_le

deleted theorem lipschitz_with.dist_inequality_of_contraction

added theorem lipschitz_with.dist_iterate_succ_le_geometric

added theorem lipschitz_with.ediam_image_le

added theorem lipschitz_with.edist_map_le

deleted theorem lipschitz_with.exists_fixed_point_of_contraction

deleted theorem lipschitz_with.fixed_point_unique_of_contraction

added theorem lipschitz_with.nndist_map_le

modified def lipschitz_with

deleted theorem uniform_continuous_of_le_add

deleted theorem uniform_continuous_of_lipschitz