Theorems · Theorem · order theory
OrderHom.nextFixed_le
∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α} (hx : x ≤ f x) {y : ↑(Function.fixedPoints ⇑f)},
x ≤ ↑y → f.nextFixed x hx ≤ y- Defined in
- Mathlib.Order.FixedPoints
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 24 from the axioms · uses propext, Quot.sound
- Assumes
- CompleteLattice
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Setstatement · cited by 53,352
- Set.Elemstatement and proof · cited by 7,166
- CompleteLatticestatement and proof · cited by 1,048
- OrderHomstatement and proof · cited by 934
- Eq.leproof · cited by 605
- sup_leproof · cited by 159
- Function.fixedPointsstatement and proof · cited by 90
- Subtype.coe_le_coeproof · cited by 20
- OrderHom.constproof · cited by 8
- OrderHom.lfp_leproof · cited by 7
- OrderHom.nextFixedstatement · cited by 4
Cited by2
Results whose statement or proof uses this declaration.
- OrderHom.nextFixed_le_iffproof · cited by 1
- OrdinalApprox.nextFixed_eq_iSup_lfpApproxproof · cited by 1