Theorems · Theorem · order theory
OmegaCompletePartialOrder.ContinuousHom.monotone
∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
(f : α →𝒄 β), Monotone ⇑f- Defined in
- Mathlib.Order.OmegaCompletePartialOrder
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 28 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- Monotonestatement · cited by 1,397
- OmegaCompletePartialOrderstatement and proof · cited by 104
- OmegaCompletePartialOrder.ContinuousHomstatement and proof · cited by 41
- OrderHom.monotone'proof · cited by 8
- OmegaCompletePartialOrder.ContinuousHom.toOrderHomproof · cited by 4
Cited by3
Results whose statement or proof uses this declaration.
- OmegaCompletePartialOrder.fixedPoints.ωSup_iterate_le_prefixedPointproof · cited by 2
- OmegaCompletePartialOrder.ContinuousHom.forall_forall_mergeproof · cited by 1
- OmegaCompletePartialOrder.ContinuousHom.ωScottContinuous_applyproof · cited by 0