Structures · Order
OmegaCompletePartialOrder
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
- Shape
- One type argument · adds ωSup, le_ωSup, ωSup_le
Extends1
Extended by2
Forgetful instances
Provided automatically by
Concrete types that are instances6
- Part
- OmegaCompletePartialOrder.ContinuousHom
- ωCPO.carrier
- Subtype
- Prod
- OrderHom
How is a type an instance?
Loading the hierarchy index…
Assumed by129
- OmegaCompletePartialOrder.ωSup
- OmegaCompletePartialOrder.ωScottContinuous
- OmegaCompletePartialOrder.ωScottContinuous.monotone
- OmegaCompletePartialOrder.ωSup_le
- OmegaCompletePartialOrder.ωScottContinuous.map_ωSup
- OmegaCompletePartialOrder.ωScottContinuous.of_monotone_map_ωSup
- OmegaCompletePartialOrder.le_ωSup
- OmegaCompletePartialOrder.ContinuousHom.comp
- OmegaCompletePartialOrder.fixedPoints.iterateChain
- OmegaCompletePartialOrder.ContinuousHom.toOrderHom
- OmegaCompletePartialOrder.ωScottContinuous.of_map_ωSup_of_orderHom
- OmegaCompletePartialOrder.ContinuousHom.toMono
- Scott.IsOpen
- OmegaCompletePartialOrder.ContinuousHom.ωSup
- OmegaCompletePartialOrder.ContinuousHom.monotone
- CompleteLattice.ωScottContinuous.sSup
- OmegaCompletePartialOrder.le_ωSup_of_le
- OmegaCompletePartialOrder.ContinuousHom.id
- OmegaCompletePartialOrder.ωScottContinuous_iff_monotone_map_ωSup
- OmegaCompletePartialOrder.ωScottContinuous_iff_map_ωSup_of_orderHom
- OmegaCompletePartialOrder.ωScottContinuous.apply₂
- OmegaCompletePartialOrder.ωScottContinuous.id
- OmegaCompletePartialOrder.ContinuousHom.continuous
- Prod.ωSupImpl
- OmegaCompletePartialOrder.ContinuousHom.Prod.apply
- OmegaCompletePartialOrder.ωScottContinuous.of_apply₂
- OmegaCompletePartialOrder.isLUB_range_ωSup
- OmegaCompletePartialOrder.ContinuousHom.ωScottContinuous.bind
- OmegaCompletePartialOrder.ωSup_eq_of_isLUB
- OmegaCompletePartialOrder.fixedPoints.ωSup_iterate_le_prefixedPoint
- OmegaCompletePartialOrder.ωScottContinuous.const
- OmegaCompletePartialOrder.ωScottContinuous.comp
- OmegaCompletePartialOrder.ContinuousHom.const
- OmegaCompletePartialOrder.ContinuousHom.flip
- CompleteLattice.ωScottContinuous.inf
- OmegaCompletePartialOrder.ContinuousHom.forall_forall_merge
- OmegaCompletePartialOrder.ContinuousHom.ωSup_apply
- OmegaCompletePartialOrder.ContinuousHom.Prod.apply_apply
- Pi.ωScottContinuous_curry
- OmegaCompletePartialOrder.ContinuousHom.seq
- OmegaCompletePartialOrder.ωSup_le_iff
- OmegaCompletePartialOrder.ContinuousHom.ωScottContinuous
- Pi.ωScottContinuous_uncurry
- CompleteLattice.ωScottContinuous.iSup
- OmegaCompletePartialOrder.ContinuousHom.bind
- OmegaCompletePartialOrder.ContinuousHom.apply_mono
- OmegaCompletePartialOrder.ωScottContinuous.map_ωSup_of_orderHom
- OmegaCompletePartialOrder.ContinuousHom.ωSup_bind
- OmegaCompletePartialOrder.ContinuousHom.copy
- OmegaCompletePartialOrder.OrderHom.ωSup