Theorems · Definition · logic and foundations
OrdinalApprox.lfpApprox
{α : Type u} → [inst : CompleteLattice α] → (α →o α) → α → Ordinal.{u} → αThe ordinal-indexed sequence approximating the least fixed point greater than
an initial value x. It is defined in such a way that we have lfpApprox 0 x = x and
lfpApprox a x = ⨆ b < a, f (lfpApprox b x).
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 40 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.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- 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
Cited by21
Results whose statement or proof uses this declaration.
- OrdinalApprox.lfpApprox_mono_rightstatement and proof · cited by 7
- OrdinalApprox.lfpApprox_zerostatement and proof · cited by 4
- OrdinalApprox.apply_lfpApprox_le_lfpApprox_of_ltstatement and proof · cited by 4
- OrdinalApprox.le_lfpApproxstatement · cited by 4
- OrdinalApprox.lfpApprox_eq_of_mem_fixedPointsstatement and proof · cited by 4
- OrdinalApprox.lfpApprox_ord_mem_fixedPointstatement and proof · cited by 3
- OrdinalApprox.lfpApprox_add_onestatement and proof · cited by 3
- OrdinalApprox.lfpApprox_le_of_mem_fixedPointsstatement and proof · cited by 3
- OrdinalApprox.lfpApprox_mem_fixedPoints_of_eqstatement and proof · cited by 3
- OrdinalApprox.lfpApprox_ord_eq_lfpstatement and proof · cited by 2
- OrdinalApprox.exists_lfpApprox_eq_lfpApproxstatement and proof · cited by 2
- OrdinalApprox.iSup_lfpApprox_eq_of_mem_fixedPointsstatement and proof · cited by 2