Structures · Order
ConditionallyCompletePartialOrderSup
Conditionally complete partial orders (with suprema) are partial orders where every nonempty, directed set which is bounded above has a least upper bound.
- Shape
- One type argument · adds isLUB_csSup_of_directed
Extends2
Extended by2
Forgetful instances
Provided automatically by
Concrete types that are instances1
- OrderDual
How is a type an instance?
Loading the hierarchy index…
Assumed by55
- ciSup_const
- ciSup_unique
- tendsto_atTop_ciSup
- IsGreatest.csSup_eq
- DirectedOn.isLUB_csSup
- DirectedOn.le_csSup
- csSup_singleton
- ciSup_pos
- csSup_Iic
- Directed.le_ciSup
- ciSup_eq_ite
- DirectedOn.csSup_le
- csSup_Icc
- Directed.ciSup_le_iff
- GaloisConnection.l_ciSup_of_directed
- GaloisConnection.l_csSup_of_directedOn
- ciSup_neg
- GaloisConnection.l_csSup_of_directedOn'
- tendsto_atBot_ciSup
- Directed.ciSup_le
- cbiSup_eq_of_forall
- cbiSup_eq_of_forall_not
- ConditionallyCompletePartialOrderSup.isLUB_csSup_of_directed
- ciSup_mem_iInter_Icc_of_antitone_Icc
- Directed.le_ciSup_of_le
- cbiSup_empty
- Directed.isLUB_ciSup
- DirectedOn.csSup_eq_of_forall_le_of_forall_lt_exists_gt
- Monotone.ciSup_mem_iInter_Icc_of_antitone
- GaloisConnection.l_ciSup_set_of_directedOn
- IsGreatest.directedOn
- ciSup_Iic
- DirectedOn.isLUB_ciSup_set
- OrderDual.instConditionallyCompletePartialOrderInfOfConditionallyCompletePartialOrderSup
- DirectedOn.notMem_of_csSup_lt
- DirectedOn.le_csSup_of_le
- DirectedOn.le_ciSup_set
- DirectedOn.csSup_le_csSup
- OrderIso.map_ciSup_set_of_directedOn
- Directed.Ici_ciSup
- ConditionallyCompletePartialOrderSup.toPartialOrder
- OrderIso.map_csSup_of_directedOn
- DirectedOn.le_csSup_iff
- DirectedOn.csSup_le_iff
- OrderIso.map_ciSup_of_directed
- DirectedOn.lt_csSup_of_lt
- Directed.ciSup_eq_of_forall_le_of_forall_lt_exists_gt
- IsGreatest.csSup_mem
- sup_eq_top_of_top_mem
- ciSup_subsingleton