Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-03 12:09 9fc24137

View on Github →

feat(order/iterate): a few more lemmas about f^[n] (#2925)

Estimated changes

Modified src/algebra/order.lean

added theorem ordering.compares_iff_of_compares_impl

Modified src/logic/function/iterate.lean

modified theorem function.iterate_id

Modified src/order/iterate.lean

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 monotone.iterate_ge_of_ge

added theorem monotone.iterate_le_of_le