Structures · Order
ConditionallyCompletePartialOrderInf
Conditionally complete partial orders (with infima) are partial orders where every nonempty, directed set which is bounded below has a greatest lower bound.
- Shape
- One type argument · adds isGLB_csInf_of_directed
Extends2
Extended by1
Concrete types that are instances1
- OrderDual
How is a type an instance?
Loading the hierarchy index…
Assumed by53
- ciInf_const
- IsLeast.csInf_eq
- ciInf_unique
- DirectedOn.csInf_le
- tendsto_atTop_ciInf
- DirectedOn.isGLB_csInf
- csInf_singleton
- csInf_Ici
- DirectedOn.le_csInf
- ciInf_pos
- Directed.ciInf_le
- GaloisConnection.u_csInf_of_directedOn'
- csInf_Icc
- Directed.le_ciInf_iff
- ciInf_eq_ite
- GaloisConnection.u_csInf_of_directedOn
- GaloisConnection.u_ciInf_of_directed
- GaloisConnection.u_ciInf_set_of_directedOn
- cbiInf_eq_of_forall_not
- DirectedOn.csInf_eq_of_forall_ge_of_forall_gt_exists_lt
- ConditionallyCompletePartialOrderInf.isGLB_csInf_of_directed
- IsLeast.directedOn
- ciInf_neg
- ciInf_subsingleton
- Directed.ciInf_le_of_le
- DirectedOn.isGLB_ciInf_set
- Directed.le_ciInf
- IsLeast.csInf_mem
- tendsto_atBot_ciInf
- Directed.isGLB_ciInf
- inf_eq_bot_of_bot_mem
- OrderIso.map_ciInf_of_directed
- OrderDual.instConditionallyCompletePartialOrderSupOfConditionallyCompletePartialOrderInf
- DirectedOn.le_ciInf_set_iff
- OrderIso.map_csInf_of_directedOn
- DirectedOn.le_csInf_iff
- ConditionallyCompletePartialOrderInf.toPartialOrder
- DirectedOn.csInf_lt_of_lt
- ConditionallyCompletePartialOrderInf.toInfSet
- ciInf_Ici
- OrderIso.map_ciInf_set_of_directedOn
- DirectedOn.ciInf_set_le
- cbiInf_eq_of_forall
- DirectedOn.csInf_le_of_le
- Directed.ciInf_mono
- Directed.ciInf_eq_of_forall_ge_of_forall_gt_exists_lt
- Directed.Iic_ciInf
- DirectedOn.csInf_le_iff
- DirectedOn.csInf_le_csInf
- csInf_Ico