Commit 2022-11-23 03:03 c5e4579d

View on Github →

feat: port Order.Iterate (#648) mathlib SHA: fd47bdf09e90f553519c712378e651975fe8c829

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Iterate.lean

added theorem Function.Commute.iterate_le_of_map_le

added theorem Function.Commute.iterate_pos_eq_iff_map_eq

added theorem Function.Commute.iterate_pos_le_iff_map_le'

added theorem Function.Commute.iterate_pos_le_iff_map_le

added theorem Function.Commute.iterate_pos_lt_iff_map_lt'

added theorem Function.Commute.iterate_pos_lt_iff_map_lt

added theorem Function.Commute.iterate_pos_lt_of_map_lt'

added theorem Function.Commute.iterate_pos_lt_of_map_lt

added theorem Function.antitone_iterate_of_le_id

added theorem Function.id_le_iterate_of_id_le

added theorem Function.iterate_le_id_of_le_id

added theorem Function.monotone_iterate_of_id_le

added theorem Monotone.antitone_iterate_of_map_le

added theorem Monotone.iterate_comp_le_of_le

added theorem Monotone.iterate_le_of_le

added theorem Monotone.le_iterate_comp_of_le

added theorem Monotone.le_iterate_of_le

added theorem Monotone.monotone_iterate_of_le_map

added theorem Monotone.seq_le_seq

added theorem Monotone.seq_lt_seq_of_le_of_lt

added theorem Monotone.seq_lt_seq_of_lt_of_le

added theorem Monotone.seq_pos_lt_seq_of_le_of_lt

added theorem Monotone.seq_pos_lt_seq_of_lt_of_le

added theorem StrictMono.strictAnti_iterate_of_map_lt

added theorem StrictMono.strictMono_iterate_of_lt_map