Theorems · Theorem · order theory
Monotone.seq_le_seq
∀ {α : Type u_1} [inst : Preorder α] {f : α → α} {x y : ℕ → α},
Monotone f → ∀ (n : ℕ), x 0 ≤ y 0 → (∀ k < n, x (k + 1) ≤ f (x k)) → (∀ k < n, f (y k) ≤ y (k + 1)) → x n ≤ y n- Defined in
- Mathlib.Order.Iterate
- Cited by
- 5 results in Mathlib
- Foundations
- Depth 21 from the axioms · uses no axioms
- Assumes
- Preorder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Preorderstatement and proof · cited by 7,952
- LE.le.transproof · cited by 3,151
- Monotonestatement and proof · cited by 1,397
- LT.lt.transproof · cited by 370
Cited by5
Results whose statement or proof uses this declaration.
- geom_leproof · cited by 2
- Function.Commute.iterate_le_of_map_leproof · cited by 2
- Monotone.le_iterate_comp_of_leproof · cited by 1
- le_geomproof · cited by 1
- Monotone.iterate_comp_le_of_leproof · cited by 1