Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-26 07:25 367d71ef

View on Github →

chore(order/iterate): review, add docs (#9965)

reorder sections;
add section docs;
use inequalities between functions in a few statements;
add a few lemmas about strict_mono functions.

Estimated changes

Modified src/order/iterate.lean

added theorem function.antitone_iterate_of_le_id

modified theorem function.id_le_iterate_of_id_le

modified theorem function.iterate_le_id_of_le_id

deleted theorem function.iterate_le_iterate_of_id_le

deleted theorem function.iterate_le_iterate_of_le_id

added theorem function.monotone_iterate_of_id_le

added theorem monotone.antitone_iterate_of_map_le

modified theorem monotone.iterate_comp_le_of_le

deleted theorem monotone.iterate_ge_of_ge

modified theorem monotone.iterate_le_of_le

modified theorem monotone.le_iterate_comp_of_le

added theorem monotone.le_iterate_of_le

added theorem monotone.monotone_iterate_of_le_map

added theorem strict_mono.strict_anti_iterate_of_map_lt

added theorem strict_mono.strict_mono_iterate_of_lt_map