Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2019-01-23 11:48
5317b593
View on Github →
refactor(contraction_mapping): add more proves about Lipschitz continuous functions; cleanup proofs
Estimated changes
Modified
src/algebra/pi_instances.lean
deleted
def
prod.prod_semilattice_sup
Modified
src/analysis/normed_space/basic.lean
deleted
theorem
squeeze_zero
Modified
src/contraction_mapping.lean
deleted
theorem
continuous_prod_snd
deleted
theorem
dist_bound_of_contraction
deleted
theorem
dist_inequality_of_contraction
deleted
theorem
fixed_point_exists_of_contraction
deleted
theorem
fixed_point_of_iteration_limit
added
theorem
fixed_point_of_tendsto_iterate
deleted
theorem
fixed_point_unique_of_contraction
deleted
theorem
iterated_lipschitz_of_lipschitz
deleted
def
lipschitz
added
theorem
lipschitz_with.dist_bound_of_contraction
added
theorem
lipschitz_with.dist_inequality_of_contraction
added
theorem
lipschitz_with.exists_fixed_point_of_contraction
added
theorem
lipschitz_with.fixed_point_unique_of_contraction
added
def
lipschitz_with
deleted
theorem
tendsto_dist_bound_at_top_nhds_0
deleted
theorem
uniform_continuous_of_lipschitz
Modified
src/order/filter.lean
Modified
src/topology/metric_space/basic.lean
deleted
theorem
dist_prod_eq_dist_0
added
theorem
metric.uniformity_eq_comap_nhds_zero
added
theorem
squeeze_zero
Modified
src/topology/uniform_space/basic.lean