Indexed

📁 Source: Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean

Statistics

Metric	Count
Definitions	0
Theorems `l_ciSup`, `l_ciSup_set`, `l_csSup`, `l_csSup'`, `u_ciInf`, `u_ciInf_set`, `u_csInf`, `u_csInf'`, `ciInf_eq`, `ciInf_set_eq`, `ciSup_eq`, `ciSup_set_eq`, `map_ciInf`, `map_ciInf_set`, `map_ciSup`, `map_ciSup'`, `map_ciSup_set`, `map_csInf`, `map_csInf'`, `map_csSup`, `map_csSup'`, `Ici_ciSup`, `Iic_ciInf`, `ciSup_empty`, `coe_biInf`, `coe_biSup`, `coe_iInf`, `coe_iSup`, `coe_iInf`, `coe_iSup`, `iInf_coe_eq_top`, `iInf_coe_lt_top`, `iInf_empty`, `iSup_coe_eq_top`, `iSup_coe_lt_top`, `cbiInf_eq_of_not_forall`, `cbiSup_eq_of_not_forall`, `ciInf_eq_bot_of_bot_mem`, `ciInf_eq_of_forall_ge_of_forall_gt_exists_lt`, `ciInf_eq_top_of_top_mem`, `ciInf_image`, `ciInf_le`, `ciInf_le'`, `ciInf_le_ciSup`, `ciInf_le_of_le`, `ciInf_le_of_le'`, `ciInf_lt_iff`, `ciInf_mem`, `ciInf_mono`, `ciInf_set_le`, `ciInf_subtype`, `ciInf_subtype'`, `ciInf_subtype''`, `ciSup_eq_of_forall_le_of_forall_lt_exists_gt`, `ciSup_false`, `ciSup_image`, `ciSup_le`, `ciSup_le'`, `ciSup_le_iff`, `ciSup_le_iff'`, `ciSup_mono`, `ciSup_mono'`, `ciSup_of_empty`, `ciSup_or'`, `ciSup_set_le_iff`, `ciSup_subtype`, `ciSup_subtype'`, `ciSup_subtype''`, `csInf_image`, `csSup_image`, `exists_lt_of_ciInf_lt`, `exists_lt_of_lt_ciSup`, `exists_lt_of_lt_ciSup'`, `isGLB_ciInf`, `isGLB_ciInf_set`, `isLUB_ciSup`, `isLUB_ciSup_set`, `le_ciInf`, `le_ciInf_iff`, `le_ciInf_iff'`, `le_ciInf_set_iff`, `le_ciSup`, `le_ciSup_iff'`, `le_ciSup_of_le`, `le_ciSup_set`, `lt_ciSup_iff`, `lt_ciSup_iff'`	87
Total	87

GaloisConnection

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`l_ciSup` 📖	mathematical	`GaloisConnection` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `BddAbove` `Preorder.toLE` `Set.range`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`iSup.eq_1` `l_csSup` `Set.range_nonempty` `iSup_range'`
`l_ciSup_set` 📖	mathematical	`GaloisConnection` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `BddAbove` `Preorder.toLE` `Set.image` `Set.Nonempty`	`iSup` `Set.Elem` `ConditionallyCompletePartialOrderSup.toSupSet` `Set` `Set.instMembership`	—	`l_ciSup` `Set.Nonempty.to_subtype` `Set.image_eq_range`
`l_csSup` 📖	mathematical	`GaloisConnection` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.Nonempty` `BddAbove` `Preorder.toLE`	`SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `iSup` `Set.Elem` `Set` `Set.instMembership`	—	`IsLUB.ciSup_set_eq` `isLUB_l_image` `isLUB_csSup`
`l_csSup'` 📖	mathematical	`GaloisConnection` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.Nonempty` `BddAbove` `Preorder.toLE`	`SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `Set.image`	—	`l_csSup` `sSup_image'`
`u_ciInf` 📖	mathematical	`GaloisConnection` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `BddBelow` `Preorder.toLE` `Set.range`	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	`l_ciSup` `dual`
`u_ciInf_set` 📖	mathematical	`GaloisConnection` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `BddBelow` `Preorder.toLE` `Set.image` `Set.Nonempty`	`iInf` `Set.Elem` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `Set` `Set.instMembership`	—	`l_ciSup_set` `dual`
`u_csInf` 📖	mathematical	`GaloisConnection` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.Nonempty` `BddBelow` `Preorder.toLE`	`InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `iInf` `Set.Elem` `Set` `Set.instMembership`	—	`l_csSup` `dual`
`u_csInf'` 📖	mathematical	`GaloisConnection` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.Nonempty` `BddBelow` `Preorder.toLE`	`InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `Set.image`	—	`l_csSup'` `dual`

IsGLB

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ciInf_eq` 📖	mathematical	`IsGLB` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.range`	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	`csInf_eq` `Set.range_nonempty`
`ciInf_set_eq` 📖	mathematical	`IsGLB` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.image` `Set.Nonempty`	`iInf` `Set.Elem` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `Set` `Set.instMembership`	—	`csInf_eq` `Set.image_eq_range` `Set.Nonempty.image`

IsLUB

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ciSup_eq` 📖	mathematical	`IsLUB` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.range`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`csSup_eq` `Set.range_nonempty`
`ciSup_set_eq` 📖	mathematical	`IsLUB` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.image` `Set.Nonempty`	`iSup` `Set.Elem` `ConditionallyCompletePartialOrderSup.toSupSet` `Set` `Set.instMembership`	—	`csSup_eq` `Set.image_eq_range` `Set.Nonempty.image`

OrderIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_ciInf` 📖	mathematical	`BddBelow` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.range`	`DFunLike.coe` `OrderIso` `instFunLikeOrderIso` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	`map_ciSup`
`map_ciInf_set` 📖	mathematical	`BddBelow` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.image` `Set.Nonempty`	`DFunLike.coe` `OrderIso` `instFunLikeOrderIso` `iInf` `Set.Elem` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `Set` `Set.instMembership`	—	`map_ciSup_set`
`map_ciSup` 📖	mathematical	`BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.range`	`DFunLike.coe` `OrderIso` `instFunLikeOrderIso` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`GaloisConnection.l_ciSup` `to_galoisConnection`
`map_ciSup'` 📖	mathematical	—	`DFunLike.coe` `OrderIso` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `instFunLikeOrderIso` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`isEmpty_or_nonempty` `ciSup_of_empty` `map_bot` `map_ciSup` `Function.Surjective.forall` `surjective` `ciSup_of_not_bddAbove` `csSup_empty`
`map_ciSup_set` 📖	mathematical	`BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.image` `Set.Nonempty`	`DFunLike.coe` `OrderIso` `instFunLikeOrderIso` `iSup` `Set.Elem` `ConditionallyCompletePartialOrderSup.toSupSet` `Set` `Set.instMembership`	—	`GaloisConnection.l_ciSup_set` `to_galoisConnection`
`map_csInf` 📖	mathematical	`Set.Nonempty` `BddBelow` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder`	`DFunLike.coe` `OrderIso` `instFunLikeOrderIso` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `iInf` `Set.Elem` `Set` `Set.instMembership`	—	`map_csSup`
`map_csInf'` 📖	mathematical	`Set.Nonempty` `BddBelow` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder`	`DFunLike.coe` `OrderIso` `instFunLikeOrderIso` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `Set.image`	—	`map_csSup'`
`map_csSup` 📖	mathematical	`Set.Nonempty` `BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder`	`DFunLike.coe` `OrderIso` `instFunLikeOrderIso` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `iSup` `Set.Elem` `Set` `Set.instMembership`	—	`GaloisConnection.l_csSup` `to_galoisConnection`
`map_csSup'` 📖	mathematical	`Set.Nonempty` `BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder`	`DFunLike.coe` `OrderIso` `instFunLikeOrderIso` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `Set.image`	—	`GaloisConnection.l_csSup'` `to_galoisConnection`

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Ici_ciSup` 📖	mathematical	`BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `range`	`Ici` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `iInter`	—	`Iic_ciInf`
`Iic_ciInf` 📖	mathematical	`BddBelow` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `range`	`Iic` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `iInter`	—	`ext` `le_ciInf_iff`

WithBot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ciSup_empty` 📖	mathematical	—	`iSup` `WithBot` `instSupSet` `Bot.bot` `bot`	—	`WithTop.iInf_empty`
`coe_biInf` 📖	mathematical	—	`some` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Set` `Set.instMembership` `WithBot` `instInfSet` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup`	—	`le_antisymm` `biInf_le` `LE.le.trans_eq` `le_iInf_iff` `iInf_pos` `iInf_neg` `coe_iInf` `OrderBot.bddBelow`
`coe_biSup` 📖	mathematical	`Set.Nonempty`	`some` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Set` `Set.instMembership` `WithBot` `instSupSet` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder`	—	`le_antisymm` `Eq.trans_le` `coe_iSup` `OrderTop.bddAbove` `iSup_le_iff` `iSup_pos` `le_biSup` `iSup_neg` `le_trans` `coe_le_coe`
`coe_iInf` 📖	mathematical	`BddBelow` `Preorder.toLE` `Set.range`	`some` `iInf` `WithBot` `instInfSet`	—	`WithTop.coe_iSup`
`coe_iSup` 📖	mathematical	`BddAbove` `Preorder.toLE` `Set.range`	`some` `iSup` `WithBot` `instSupSet`	—	`WithTop.coe_iInf`

WithTop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_iInf` 📖	mathematical	`BddBelow` `Preorder.toLE` `Set.range`	`some` `iInf` `WithTop` `instInfSet`	—	`iInf.eq_1` `coe_sInf'` `Set.range_nonempty` `Set.range_comp`
`coe_iSup` 📖	mathematical	`BddAbove` `Preorder.toLE` `Set.range`	`some` `iSup` `WithTop` `instSupSet`	—	`iSup.eq_1` `coe_sSup'` `Set.range_comp`
`iInf_coe_eq_top` 📖	mathematical	—	`iInf` `WithTop` `instInfSet` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `some` `Top.top` `top` `IsEmpty`	—	—
`iInf_coe_lt_top` 📖	mathematical	—	`WithTop` `Preorder.toLT` `instPreorder` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `iInf` `instInfSet` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `some` `Top.top` `top`	—	`lt_top_iff_ne_top` `iInf_coe_eq_top` `not_isEmpty_iff`
`iInf_empty` 📖	mathematical	—	`iInf` `WithTop` `instInfSet` `Top.top` `top`	—	`iInf.eq_1` `Set.range_eq_empty` `sInf_empty`
`iSup_coe_eq_top` 📖	mathematical	—	`iSup` `WithTop` `instSupSet` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `ConditionallyCompletePartialOrderSup.toSupSet` `some` `Top.top` `top` `BddAbove` `Preorder.toLE` `Set.range`	—	`iSup_eq_top` `not_bddAbove_iff` `coe_lt_top` `coe_lt_coe` `LT.lt.ne` `coe_untop`
`iSup_coe_lt_top` 📖	mathematical	—	`WithTop` `Preorder.toLT` `instPreorder` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `iSup` `instSupSet` `ConditionallyCompletePartialOrderSup.toSupSet` `some` `Top.top` `top` `BddAbove` `Preorder.toLE` `Set.range`	—	`lt_top_iff_ne_top` `Iff.not_left` `iSup_coe_eq_top`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cbiInf_eq_of_not_forall` 📖	mathematical	—	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `InfSet.sInf` `Set` `Set.instEmptyCollection`	—	`cbiSup_eq_of_not_forall`
`cbiSup_eq_of_not_forall` 📖	mathematical	—	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `SupSet.sSup` `Set` `Set.instEmptyCollection`	—	`ciSup_eq_ite` `Set.mem_range_self` `le_antisymm` `ciSup_le` `le_ciSup` `sup_le` `isEmpty_or_nonempty` `iSup_of_empty'` `csSup_of_not_bddAbove` `sup_of_le_left` `Mathlib.Tactic.Contrapose.contrapose₄` `BddAbove.mono` `Subtype.coe_eta`
`ciInf_eq_bot_of_bot_mem` 📖	mathematical	`Set` `Set.instMembership` `Set.range` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	`csInf_eq_bot_of_bot_mem`
`ciInf_eq_of_forall_ge_of_forall_gt_exists_lt` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Preorder.toLT`	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	`ciSup_eq_of_forall_le_of_forall_lt_exists_gt`
`ciInf_eq_top_of_top_mem` 📖	mathematical	`Set` `Set.instMembership` `Set.range` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`csSup_eq_top_of_top_mem`
`ciInf_image` 📖	mathematical	`Set.Nonempty` `BddBelow` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.range` `Set.Elem` `Set` `Set.instMembership` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `InfSet.sInf` `Set.instEmptyCollection`	`Set.image`	—	`ciSup_image`
`ciInf_le` 📖	mathematical	`BddBelow` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.range`	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	`le_ciSup`
`ciInf_le'` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	`ciInf_le` `OrderBot.bddBelow`
`ciInf_le_ciSup` 📖	mathematical	`BddBelow` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.range` `BddAbove`	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`LE.le.trans` `ciInf_le` `le_ciSup`
`ciInf_le_of_le` 📖	mathematical	`BddBelow` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.range`	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	`le_ciSup_of_le`
`ciInf_le_of_le'` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder`	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	`ciInf_le_of_le` `OrderBot.bddBelow`
`ciInf_lt_iff` 📖	mathematical	`BddBelow` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Set.range`	`Preorder.toLT` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	`csInf_lt_iff` `Set.range_nonempty`
`ciInf_mem` 📖	mathematical	—	`Set` `Set.instMembership` `Set.range` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`csInf_mem` `Set.range_nonempty`
`ciInf_mono` 📖	mathematical	`BddBelow` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.range`	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	`ciSup_mono`
`ciInf_set_le` 📖	mathematical	`BddBelow` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.image` `Set` `Set.instMembership`	`iInf` `Set.Elem` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	`le_ciSup_set`
`ciInf_subtype` 📖	—	`BddBelow` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.range` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `InfSet.sInf` `Set` `Set.instEmptyCollection`	—	—	`ciSup_subtype`
`ciInf_subtype'` 📖	—	`BddBelow` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.range` `Subtype.prop` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `InfSet.sInf` `Set` `Set.instEmptyCollection`	—	—	`Subtype.prop` `ciInf_subtype`
`ciInf_subtype''` 📖	—	`Set.Nonempty` `BddBelow` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.range` `Set.Elem` `Set` `Set.instMembership` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `InfSet.sInf` `Set.instEmptyCollection`	—	—	`ciInf_subtype` `Set.Nonempty.to_subtype`
`ciSup_eq_of_forall_le_of_forall_lt_exists_gt` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Preorder.toLT`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`csSup_eq_of_forall_le_of_forall_lt_exists_gt` `Set.range_nonempty` `Set.forall_mem_range` `Set.exists_range_iff`
`ciSup_false` 📖	mathematical	—	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrderBot.toOrderBot`	—	`ciSup_of_empty` `instIsEmptyFalse`
`ciSup_image` 📖	mathematical	`Set.Nonempty` `BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.range` `Set.Elem` `Set` `Set.instMembership` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `Set.instEmptyCollection` `iSup`	`Set.image`	—	`LE.le.trans` `Set.Nonempty.to_subtype` `ciSup_le` `Set.mem_image_of_mem` `le_ciSup_set` `Subtype.prop` `csSup_image` `Set.image_comp`
`ciSup_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`csSup_le` `Set.range_nonempty` `Set.forall_mem_range`
`ciSup_le'` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`csSup_le'` `Set.forall_mem_range`
`ciSup_le_iff` 📖	mathematical	`BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.range`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`isLUB_le_iff` `isLUB_ciSup` `Set.forall_mem_range`
`ciSup_le_iff'` 📖	mathematical	`BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Set.range`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`csSup_le_iff'` `Set.forall_mem_range`
`ciSup_mono` 📖	mathematical	`BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.range`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`isEmpty_or_nonempty` `iSup_of_empty'` `le_refl` `ciSup_le` `le_ciSup_of_le`
`ciSup_mono'` 📖	mathematical	`BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Set.range`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`ciSup_le'` `le_ciSup_of_le`
`ciSup_of_empty` 📖	mathematical	—	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrderBot.toOrderBot`	—	`iSup_of_empty'` `csSup_empty`
`ciSup_or'` 📖	mathematical	—	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice`	—	`iSup_congr_Prop` `ciSup_unique` `max_self` `ciSup_of_empty` `instIsEmptyFalse` `sup_of_le_left` `sup_of_le_right`
`ciSup_set_le_iff` 📖	mathematical	`Set.Nonempty` `BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.image`	`iSup` `Set.Elem` `ConditionallyCompletePartialOrderSup.toSupSet` `Set` `Set.instMembership`	—	`isLUB_le_iff` `isLUB_ciSup_set` `Set.forall_mem_image`
`ciSup_subtype` 📖	—	`BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.range` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `Set` `Set.instEmptyCollection` `iSup`	—	—	`le_antisymm` `ciSup_le` `iSup_congr_Prop` `ciSup_unique` `le_ciSup` `ciSup_eq_ite` `BddAbove.mono` `Set.union_singleton` `BddAbove.union` `SemilatticeSup.instIsDirectedOrder` `bddAbove_singleton`
`ciSup_subtype'` 📖	—	`BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.range` `Subtype.prop` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `Set` `Set.instEmptyCollection` `iSup`	—	—	`Subtype.prop` `ciSup_subtype`
`ciSup_subtype''` 📖	—	`Set.Nonempty` `BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.range` `Set.Elem` `Set` `Set.instMembership` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `Set.instEmptyCollection` `iSup`	—	—	`ciSup_subtype` `Set.Nonempty.to_subtype`
`csInf_image` 📖	mathematical	`Set.Nonempty` `BddBelow` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.range` `Set.Elem` `Set` `Set.instMembership` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `InfSet.sInf` `Set.instEmptyCollection`	`Set.image`	—	`csSup_image`
`csSup_image` 📖	mathematical	`Set.Nonempty` `BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.range` `Set.Elem` `Set` `Set.instMembership` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `Set.instEmptyCollection` `iSup`	`Set.image`	—	`ciSup_subtype''` `iSup.eq_1` `Set.image_eq_range`
`exists_lt_of_ciInf_lt` 📖	—	`Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	—	`exists_lt_of_lt_ciSup`
`exists_lt_of_lt_ciSup` 📖	—	`Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	—	`exists_lt_of_lt_csSup` `Set.range_nonempty`
`exists_lt_of_lt_ciSup'` 📖	—	`Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	—	`Mathlib.Tactic.Contrapose.contrapose₁` `ciSup_le'`
`isGLB_ciInf` 📖	mathematical	`BddBelow` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.range`	`IsGLB` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	`isGLB_csInf` `Set.range_nonempty`
`isGLB_ciInf_set` 📖	mathematical	`BddBelow` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.image` `Set.Nonempty`	`IsGLB` `iInf` `Set.Elem` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `Set` `Set.instMembership`	—	`isLUB_ciSup_set`
`isLUB_ciSup` 📖	mathematical	`BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.range`	`IsLUB` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`isLUB_csSup` `Set.range_nonempty`
`isLUB_ciSup_set` 📖	mathematical	`BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.image` `Set.Nonempty`	`IsLUB` `iSup` `Set.Elem` `ConditionallyCompletePartialOrderSup.toSupSet` `Set` `Set.instMembership`	—	`sSup_image'` `isLUB_csSup` `Set.Nonempty.image`
`le_ciInf` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder`	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	`ciSup_le`
`le_ciInf_iff` 📖	mathematical	`BddBelow` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.range`	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	`le_isGLB_iff` `isGLB_ciInf` `Set.forall_mem_range`
`le_ciInf_iff'` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	`le_ciInf_iff` `OrderBot.bddBelow`
`le_ciInf_set_iff` 📖	mathematical	`Set.Nonempty` `BddBelow` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.image`	`iInf` `Set.Elem` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `Set` `Set.instMembership`	—	`le_isGLB_iff` `isGLB_ciInf_set` `Set.forall_mem_image`
`le_ciSup` 📖	mathematical	`BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.range`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`le_csSup` `Set.mem_range_self`
`le_ciSup_iff'` 📖	mathematical	`BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Set.range`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	—
`le_ciSup_of_le` 📖	mathematical	`BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.range`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`le_trans` `le_ciSup`
`le_ciSup_set` 📖	mathematical	`BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.image` `Set` `Set.instMembership`	`iSup` `Set.Elem` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`LE.le.trans_eq` `le_csSup` `Set.mem_image_of_mem` `sSup_image'`
`lt_ciSup_iff` 📖	mathematical	`BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Set.range`	`Preorder.toLT` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`lt_csSup_iff` `Set.range_nonempty`
`lt_ciSup_iff'` 📖	mathematical	`BddAbove` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Set.range`	`Preorder.toLT` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`Iff.not` `ciSup_le_iff'`

---

← Back to Index