Theorems · Definition · order theory
OmegaCompletePartialOrder.fixedPoints.iterateChain
{α : Type u_2} →
[inst : OmegaCompletePartialOrder α] → (f : α →o α) → (x : α) → x ≤ f x → OmegaCompletePartialOrder.Chain αIteration of a function on an initial element interpreted as a chain.
- Defined in
- Mathlib.Order.OmegaCompletePartialOrder
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 27 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- OmegaCompletePartialOrder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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
- OrderHomstatement and proof · cited by 934
- Nat.iterateproof · cited by 740
- OmegaCompletePartialOrderstatement and proof · cited by 104
- OmegaCompletePartialOrder.Chainstatement · cited by 85
Cited by4
Results whose statement or proof uses this declaration.
- OmegaCompletePartialOrder.fixedPoints.ωSup_iterate_le_prefixedPointstatement and proof · cited by 2
- OmegaCompletePartialOrder.fixedPoints.ωSup_iterate_mem_fixedPointstatement and proof · cited by 1
- OmegaCompletePartialOrder.fixedPoints.iterateChain.congr_simpstatement and proof · cited by 0
- OmegaCompletePartialOrder.fixedPoints.ωSup_iterate_le_fixedPointstatement · cited by 0