Theorems · Theorem · logic and foundations
OrdinalApprox.lfpApprox_eq_all_of_fixedPoint
∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α},
x ≤ f x → ((∀ (o : Ordinal.{u}), OrdinalApprox.lfpApprox f x o = x) ↔ f x = x)- Cited by
- 2 results in Mathlib
- Foundations
- Depth 45 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.
Cites12
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
- zero_addproof · cited by 2,366
- Ordinalstatement and proof · cited by 1,688
- CompleteLatticestatement and proof · cited by 1,048
- OrderHomstatement and proof · cited by 934
- zero_leproof · cited by 382
- Function.fixedPointsproof · cited by 90
- OrdinalApprox.lfpApproxstatement and proof · cited by 21
- Function.mem_fixedPoints_iffproof · cited by 16
- OrdinalApprox.lfpApprox_zeroproof · cited by 4
- OrdinalApprox.lfpApprox_eq_of_mem_fixedPointsproof · cited by 4
- OrdinalApprox.lfpApprox_add_oneproof · cited by 3
Cited by2
Results whose statement or proof uses this declaration.
- OrdinalApprox.lfpApprox_eq_of_fixedPoint_or_zeroproof · cited by 1
- OrdinalApprox.gfpApprox_eq_all_of_fixedPointproof · cited by 1