Mathlib Map

Structures · Order

ConditionallyCompletePartialOrder

Conditionally complete partial orders (with suprema and infima) are partial orders where every nonempty, directed set which is bounded above (respectively, below) has a least upper (respectively, greatest lower) bound.

Defined in
Mathlib.Order.ConditionallyCompletePartialOrder.Defs
Shape
One type argument · adds isGLB_csInf_of_directed

Extends2

Extended by1

Forgetful instances

Provided automatically by

Concrete types that are instances1

  • OrderDual

How is a type an instance?

Loading the hierarchy index…

Assumed by8

Ancestors13