Theorems · Theorem · logic and foundations
OrdinalApprox.lfpApprox_add_one
∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α},
x ≤ f x → ∀ (a : Ordinal.{u}), OrdinalApprox.lfpApprox f x (a + 1) = f (OrdinalApprox.lfpApprox f x a)- Cited by
- 3 results in Mathlib
- Foundations
- Depth 44 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CompleteLattice
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
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
- LE.le.transproof · cited by 3,151
- iSupproof · cited by 2,415
- Ordinalstatement and proof · cited by 1,688
- CompleteLatticestatement and proof · cited by 1,048
- OrderHomstatement and proof · cited by 934
- iSup_congr_Propproof · cited by 247
- sup_leproof · cited by 159
- lt_add_oneproof · cited by 105
- LE.le.antisymm'proof · cited by 104
- OrderHom.monotoneproof · cited by 70
- Monotone.compproof · cited by 67
Cited by3
Results whose statement or proof uses this declaration.
- OrdinalApprox.lfpApprox_mem_fixedPoints_of_eqproof · cited by 3
- OrdinalApprox.lfpApprox_eq_all_of_fixedPointproof · cited by 2
- OrdinalApprox.gfpApprox_add_oneproof · cited by 1