Theorems · Theorem · logic and foundations
OrdinalApprox.prevFixed_eq_iInf_gfpApprox
∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α} (hx : f x ≤ x),
↑(f.prevFixed x hx) = ⨅ a, OrdinalApprox.gfpApprox f x aThe ordinal-indexed infimum of gfpApprox equals prevFixed: the greatest fixed point
less than or equal to x.
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 83 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.
Cites11
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
- iInfstatement · cited by 1,690
- Ordinalstatement · cited by 1,688
- CompleteLatticestatement and proof · cited by 1,048
- OrderHomstatement and proof · cited by 934
- Function.fixedPointsstatement · cited by 90
- OrderHom.dualproof · cited by 48
- OrdinalApprox.gfpApproxstatement · cited by 23
- OrderHom.prevFixedstatement · cited by 4
- OrdinalApprox.nextFixed_eq_iSup_lfpApproxproof · cited by 1
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.