Commit 2020-12-15 01:31 8de08f72
View on Github →chore(order/iterate): generalize lemmas about inequalities and iterations (#5357)
If f : α → α is a monotone function and x y : ℕ → α are two
sequences such that x 0 ≤ y 0, x (n + 1) ≤ f (x n), and
f (y n) ≤ y (n + 1), then x n ≤ y n. This lemma (and its versions
for <) generalize geom_le as well as iterate_le_of_map_le.