Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-05-29 20:46 b2f643e9

View on Github →

feat(dynamics/fixed_points): define is_fixed_pt (#2857) Define function.is_fixed_pt and prove some basic properties.

Estimated changes

Modified src/analysis/calculus/inverse.lean

Created src/dynamics/fixed_points.lean

added theorem function.bij_on_fixed_pts_comp

added theorem function.commute.inv_on_fixed_pts_comp

added theorem function.commute.left_bij_on_fixed_pts_comp

added theorem function.commute.right_bij_on_fixed_pts_comp

added def function.fixed_points

added theorem function.inv_on_fixed_pts_comp

added theorem function.is_fixed_pt.left_of_comp

added theorem function.is_fixed_pt.to_left_inverse

added def function.is_fixed_pt

added theorem function.is_fixed_pt_id

added theorem function.maps_to_fixed_pts_comp

added theorem function.mem_fixed_points

added theorem function.semiconj.maps_to_fixed_pts

Modified src/logic/function/iterate.lean

added theorem function.commute.comp_iterate

added theorem function.commute.iterate_iterate_self

added theorem function.commute.iterate_self

added theorem function.commute.self_iterate

added theorem function.comp_iterate_pred_of_pos

added theorem function.iterate_pred_comp_of_pos

Modified src/order/fixed_points.lean

deleted def fixed_points

Modified src/topology/metric_space/contracting.lean

modified theorem contracting_with.dist_le_of_fixed_point

deleted theorem contracting_with.efixed_point_is_fixed'

deleted theorem contracting_with.efixed_point_is_fixed

added theorem contracting_with.efixed_point_is_fixed_pt'

added theorem contracting_with.efixed_point_is_fixed_pt

deleted theorem contracting_with.fixed_point_is_fixed

added theorem contracting_with.fixed_point_is_fixed_pt

modified theorem contracting_with.fixed_point_unique'

modified theorem contracting_with.fixed_point_unique

deleted theorem fixed_point_of_tendsto_iterate

added theorem is_fixed_pt_of_tendsto_iterate