Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2019-01-23 11:48
96198b98
View on Github →
feat(contraction_mapping): proof the Banach fixed-point theorem (closes
#553
)
Estimated changes
Modified
src/algebra/pi_instances.lean
added
def
prod.prod_semilattice_sup
Created
src/contraction_mapping.lean
added
theorem
continuous_prod_snd
added
theorem
dist_bound_of_contraction
added
theorem
dist_inequality_of_contraction
added
theorem
fixed_point_exists_of_contraction
added
theorem
fixed_point_of_iteration_limit
added
theorem
fixed_point_unique_of_contraction
added
theorem
iterated_lipschitz_of_lipschitz
added
def
lipschitz
added
theorem
tendsto_dist_bound_at_top_nhds_0
added
theorem
uniform_continuous_of_lipschitz
Modified
src/data/prod.lean
added
theorem
prod.map_def
Modified
src/order/filter.lean
added
theorem
filter.prod_at_top_at_top_eq
added
theorem
filter.prod_map_at_top_eq
Modified
src/topology/metric_space/basic.lean
added
theorem
cauchy_seq_iff_tendsto_dist_at_top_0
added
theorem
dist_prod_eq_dist_0
Modified
src/topology/uniform_space/basic.lean
added
theorem
cauchy_seq_iff_prod_map