Theorems · Theorem · logic and foundations
OrdinalApprox.lfpApprox_mono_right
∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α}, Monotone (OrdinalApprox.lfpApprox f x)- Cited by
- 7 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.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- iSupproof · cited by 2,415
- Ordinalstatement and proof · cited by 1,688
- Monotonestatement · cited by 1,397
- CompleteLatticestatement and proof · cited by 1,048
- OrderHomstatement and proof · cited by 934
- OrdinalApprox.lfpApproxstatement and proof · cited by 21
- sup_le_sup_leftproof · cited by 20
- iSup₂_mono'proof · cited by 10
Cited by7
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_mem_fixedPoints_of_eqproof · cited by 3
- OrdinalApprox.gfpApprox_anti_rightproof · cited by 2
- OrdinalApprox.iSup_lfpApprox_eq_of_mem_fixedPointsproof · cited by 2
- OrdinalApprox.lfpApprox_of_isSuccLimitproof · cited by 1
- OrdinalApprox.lfpApprox_monotoneproof · cited by 0