Theorems · Theorem · logic and foundations
OrdinalApprox.apply_lfpApprox_le_lfpApprox_of_lt
∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α} {a b : Ordinal.{u}},
a < b → f (OrdinalApprox.lfpApprox f x a) ≤ OrdinalApprox.lfpApprox f x b- Cited by
- 4 results in Mathlib
- Foundations
- Depth 43 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.
Cites8
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
- Ordinalstatement and proof · cited by 1,688
- le_rflproof · cited by 1,558
- CompleteLatticestatement and proof · cited by 1,048
- OrderHomstatement and proof · cited by 934
- le_iSup₂_of_leproof · cited by 52
- OrdinalApprox.lfpApproxstatement and proof · cited by 21
- le_sup_of_le_rightproof · cited by 17
Cited by4
Results whose statement or proof uses this declaration.
- OrdinalApprox.lfpApprox_eq_of_mem_fixedPointsproof · cited by 4
- OrdinalApprox.lfpApprox_add_oneproof · cited by 3
- OrdinalApprox.lfpApprox_of_isSuccLimitproof · cited by 1
- OrdinalApprox.gfpApprox_le_apply_gfpApprox_of_ltproof · cited by 0