Theorems · Definition · logic and foundations
OrdinalApprox.gfpApprox
{α : Type u} → [inst : CompleteLattice α] → (α →o α) → α → Ordinal.{u} → αThe ordinal-indexed sequence approximating the greatest fixed point greater than
an initial value x. It is defined in such a way that we have gfpApprox 0 x = x and
gfpApprox a x = ⨅ b < a, f (lfpApprox b x).
- Cited by
- 23 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
- iInfproof · cited by 1,690
- Ordinalstatement and proof · cited by 1,688
- CompleteLatticestatement and proof · cited by 1,048
- OrderHomstatement and proof · cited by 934
Cited by24
Results whose statement or proof uses this declaration.
- CantorBendixson.iteratedDerivedSetproof · cited by 13
- OrdinalApprox.gfpApprox_anti_rightstatement · cited by 2
- OrdinalApprox.gfpApprox_add_onestatement · cited by 1
- OrdinalApprox.gfpApprox_eq_all_of_fixedPointstatement · cited by 1
- OrdinalApprox.gfpApprox_eq_of_mem_fixedPointsstatement and proof · cited by 1
- OrdinalApprox.gfpApprox_mono_midstatement · cited by 1
- OrdinalApprox.gfpApprox_of_isSuccLimitstatement · cited by 1
- OrdinalApprox.gfpApprox_ord_mem_fixedPointstatement · cited by 1
- OrdinalApprox.gfpApprox_zerostatement · cited by 1
- CantorBendixson.iteratedDerivedSet_constant_iff_preperfectproof · cited by 1
- CantorBendixson.iteratedDerivedSet_limitproof · cited by 1
- OrdinalApprox.prevFixed_eq_iInf_gfpApproxstatement · cited by 0