Theorems · Theorem · logic and foundations
OrdinalApprox.lfpApprox_of_isSuccLimit
∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α} {a : Ordinal.{u}},
Order.IsSuccLimit a → OrdinalApprox.lfpApprox f x a = ⨆ b, OrdinalApprox.lfpApprox f x ↑b- Cited by
- 1 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.
Cites22
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Set.Elemstatement and proof · cited by 7,166
- iSupstatement and proof · cited by 2,415
- LT.lt.leproof · cited by 2,189
- Ordinalstatement and proof · cited by 1,688
- Set.Iiostatement and proof · cited by 1,166
- CompleteLatticestatement and proof · cited by 1,048
- OrderHomstatement and proof · cited by 934
- Order.IsSuccLimitstatement and proof · cited by 255
- iSup_leproof · cited by 190
- lt_add_oneproof · cited by 105
- LE.le.antisymm'proof · cited by 104
Cited by1
Results whose statement or proof uses this declaration.
- OrdinalApprox.gfpApprox_of_isSuccLimitproof · cited by 1