Commit 2023-04-10 15:18 dcfb64b3

View on Github →

feat: port Topology.MetricSpace.Contracting (#3323)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/MetricSpace/Contracting.lean

added theorem ContractingWith.aposteriori_dist_iterate_fixedPoint_le

added theorem ContractingWith.apriori_dist_iterate_fixedPoint_le

added theorem ContractingWith.apriori_edist_iterate_efixedPoint_le'

added theorem ContractingWith.apriori_edist_iterate_efixedPoint_le

added theorem ContractingWith.dist_fixedPoint_fixedPoint_of_dist_le'

added theorem ContractingWith.dist_fixedPoint_le

added theorem ContractingWith.dist_inequality

added theorem ContractingWith.dist_le_mul

added theorem ContractingWith.dist_le_of_fixedPoint

added theorem ContractingWith.edist_efixedPoint_le'

added theorem ContractingWith.edist_efixedPoint_le

added theorem ContractingWith.edist_efixedPoint_lt_top'

added theorem ContractingWith.edist_efixedPoint_lt_top

added theorem ContractingWith.edist_inequality

added theorem ContractingWith.edist_le_of_fixedPoint

added theorem ContractingWith.efixedPoint_eq_of_edist_lt_top'

added theorem ContractingWith.efixedPoint_eq_of_edist_lt_top

added theorem ContractingWith.efixedPoint_isFixedPt

added theorem ContractingWith.efixedPoint_is_fixed_pt'

added theorem ContractingWith.efixedPoint_mem'

added theorem ContractingWith.eq_or_edist_eq_top_of_fixedPoints

added theorem ContractingWith.exists_fixedPoint'

added theorem ContractingWith.exists_fixedPoint

added theorem ContractingWith.fixedPoint_isFixedPt

added theorem ContractingWith.fixedPoint_lipschitz_in_map

added theorem ContractingWith.fixedPoint_unique'

added theorem ContractingWith.fixedPoint_unique

added theorem ContractingWith.isFixedPt_fixedPoint_iterate

added theorem ContractingWith.one_sub_K_ne_top

added theorem ContractingWith.one_sub_K_ne_zero

added theorem ContractingWith.one_sub_K_pos'

added theorem ContractingWith.one_sub_K_pos

added theorem ContractingWith.restrict

added theorem ContractingWith.tendsto_iterate_efixedPoint'

added theorem ContractingWith.tendsto_iterate_efixedPoint

added theorem ContractingWith.tendsto_iterate_fixedPoint

added theorem ContractingWith.toLipschitzWith

added def ContractingWith