Theorems · Theorem · order theory
Function.Commute.iterate_le_of_map_le
∀ {α : Type u_1} [inst : Preorder α] {f g : α → α},
Function.Commute f g → Monotone f → Monotone g → ∀ {x : α}, f x ≤ g x → ∀ (n : ℕ), f^[n] x ≤ g^[n] x- Defined in
- Mathlib.Order.Iterate
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 22 from the axioms · uses propext, Quot.sound
- Assumes
- Preorder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
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_reflproof · cited by 2,061
- Monotonestatement and proof · cited by 1,397
- Nat.iteratestatement and proof · cited by 740
- Function.iterate_succ_apply'proof · cited by 72
- Function.Commutestatement and proof · cited by 54
- Function.Commute.iterate_rightproof · cited by 8
- Monotone.seq_le_seqproof · cited by 5
- Monotone.iterateproof · cited by 3
Cited by2
Results whose statement or proof uses this declaration.
- CircleDeg1Lift.le_iterate_of_add_int_le_mapproof · cited by 2
- CircleDeg1Lift.iterate_le_of_map_le_add_intproof · cited by 1