Theorems · Inductive type · order theory
OmegaCompletePartialOrder
Type u_6 → Type u_6
An omega-complete partial order is a partial order with a supremum
operation on increasing sequences indexed by natural numbers (which we
call ωSup). In this sense, it is strictly weaker than join complete
semi-lattices as only ω-sized totally ordered sets have a supremum.
See the definition on page 114 of [gunter1992].
- Defined in
- Mathlib.Order.OmegaCompletePartialOrder
- Cited by
- 104 results in Mathlib
- Foundations
- Depth 0 from the axioms, rests on 1 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by152
Results whose statement or proof uses this declaration.
- OmegaCompletePartialOrder.ωSupstatement and proof · cited by 48
- OmegaCompletePartialOrder.ωScottContinuousstatement and proof · cited by 47
- OmegaCompletePartialOrder.ContinuousHomstatement · cited by 41
- OmegaCompletePartialOrder.ωScottContinuous.monotonestatement and proof · cited by 15
- OmegaCompletePartialOrder.ωSup_lestatement and proof · cited by 11
- OmegaCompletePartialOrder.ωScottContinuous.map_ωSupstatement and proof · cited by 11
- OmegaCompletePartialOrder.ωScottContinuous.of_monotone_map_ωSupstatement and proof · cited by 9
- OmegaCompletePartialOrder.le_ωSupstatement and proof · cited by 8
- Scott.IsOpenstatement and proof · cited by 4
- OmegaCompletePartialOrder.ContinuousHom.compstatement and proof · cited by 4
- OmegaCompletePartialOrder.ContinuousHom.toMonostatement and proof · cited by 4
- OmegaCompletePartialOrder.ContinuousHom.toOrderHomstatement and proof · cited by 4