Documentation Verification Report

Finset

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

Statistics

Metric	Count
Definitions	0
Theorems `ciSup_eq_max'_image`, `ciSup_mem_image`, `csInf_eq_min'`, `csInf_mem`, `csSup_eq_max'`, `csSup_mem`, `ciInf_eq_min'_image`, `ciInf_mem_image`, `ciSup_eq_max'_image`, `ciSup_mem_image`, `inf'_eq_csInf_image`, `inf'_id_eq_csInf`, `inf'_univ_eq_ciInf`, `sup'_eq_csSup_image`, `sup'_id_eq_csSup`, `sup'_univ_eq_ciSup`, `sup_univ_eq_ciSup`, `iInf_mem_map_of_exists_le_sInf_empty`, `iSup_mem_map_of_exists_sSup_empty_le`, `iSup_mem_map_of_ne_nil`, `iInf_mem_map_of_exists_le_sInf_empty`, `iSup_mem_map_of_exists_sSup_empty_le`, `iSup_mem_map_of_ne_zero`, `ciInf_mem_image`, `ciSup_lt_iff`, `ciSup_mem_image`, `csSup_lt_iff`, `lt_ciInf_iff`, `lt_csInf_iff`, `ciSup_lt_iff`, `ciSup_mem_image`, `csInf_mem`, `csSup_mem`, `exists_eq_ciInf_of_finite`, `exists_eq_ciSup_of_finite`	35
Total	35

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ciInf_eq_min'_image` 📖	mathematical	`Finset` `SetLike.instMembership` `instSetLike` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `Set` `Set.instEmptyCollection` `Nonempty` `image` `LinearOrder.toDecidableEq` `ConditionallyCompleteLinearOrder.toLinearOrder`	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Finset` `SetLike.instMembership` `instSetLike` `min'` `ConditionallyCompleteLinearOrder.toLinearOrder` `image` `LinearOrder.toDecidableEq`	—	`Nonempty.image` `toDual_min'` `toDual_iInf` `image_nonempty` `ciSup_eq_max'_image` `image_image` `max'.congr_simp`
`ciInf_mem_image` 📖	mathematical	`Finset` `SetLike.instMembership` `instSetLike` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `Set` `Set.instEmptyCollection`	`Finset` `SetLike.instMembership` `instSetLike` `image` `LinearOrder.toDecidableEq` `ConditionallyCompleteLinearOrder.toLinearOrder` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`image_nonempty` `ciInf_eq_min'_image` `min'_mem`
`ciSup_eq_max'_image` 📖	mathematical	`Finset` `SetLike.instMembership` `instSetLike` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `Set` `Set.instEmptyCollection` `Nonempty` `image` `LinearOrder.toDecidableEq` `ConditionallyCompleteLinearOrder.toLinearOrder`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Finset` `SetLike.instMembership` `instSetLike` `max'` `ConditionallyCompleteLinearOrder.toLinearOrder` `image` `LinearOrder.toDecidableEq`	—	`iSup.eq_1` `Nonempty.csSup_eq_max'` `coe_image` `csSup_eq_csSup_of_forall_exists_le` `ciSup_eq_ite` `le_rfl` `instReflLe`
`ciSup_mem_image` 📖	mathematical	`Finset` `SetLike.instMembership` `instSetLike` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `Set` `Set.instEmptyCollection`	`Finset` `SetLike.instMembership` `instSetLike` `image` `LinearOrder.toDecidableEq` `ConditionallyCompleteLinearOrder.toLinearOrder` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`image_nonempty` `ciSup_eq_max'_image` `max'_mem`
`inf'_eq_csInf_image` 📖	mathematical	`Nonempty`	`inf'` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.image` `SetLike.coe` `Finset` `instSetLike`	—	`sup'_eq_csSup_image`
`inf'_id_eq_csInf` 📖	mathematical	`Nonempty`	`inf'` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `SetLike.coe` `Finset` `instSetLike`	—	`sup'_id_eq_csSup`
`inf'_univ_eq_ciInf` 📖	mathematical	—	`inf'` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `univ` `univ_nonempty` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder`	—	`univ_nonempty` `inf'_eq_csInf_image` `coe_univ` `Set.image_univ`
`sup'_eq_csSup_image` 📖	mathematical	`Nonempty`	`sup'` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Set.image` `SetLike.coe` `Finset` `instSetLike`	—	`eq_of_forall_ge_iff` `csSup_le_iff` `Set.Finite.bddAbove` `SemilatticeSup.instIsDirectedOrder` `supSet_to_nonempty` `Set.Finite.image` `finite_toSet` `Set.Nonempty.image` `Nonempty.to_set`
`sup'_id_eq_csSup` 📖	mathematical	`Nonempty`	`sup'` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `SetLike.coe` `Finset` `instSetLike`	—	`sup'_eq_csSup_image` `Set.image_id`
`sup'_univ_eq_ciSup` 📖	mathematical	—	`sup'` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `univ` `univ_nonempty` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder`	—	`univ_nonempty` `sup'_eq_csSup_image` `coe_univ` `Set.image_univ`
`sup_univ_eq_ciSup` 📖	mathematical	—	`sup` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `ConditionallyCompleteLinearOrderBot.toOrderBot` `univ` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder`	—	`le_antisymm` `sup_le` `le_ciSup` `Set.Finite.bddAbove` `SemilatticeSup.instIsDirectedOrder` `bot_nonempty` `Set.finite_range` `Finite.of_fintype` `ciSup_le'` `le_sup` `mem_univ`

Finset.Nonempty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ciSup_eq_max'_image` 📖	mathematical	`Finset.Nonempty` `Finset.image` `LinearOrder.toDecidableEq` `ConditionallyCompleteLinearOrder.toLinearOrder` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `image`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.max'` `ConditionallyCompleteLinearOrder.toLinearOrder` `Finset.image` `LinearOrder.toDecidableEq`	—	`Finset.ciSup_eq_max'_image` `csSup_empty`
`ciSup_mem_image` 📖	mathematical	`Finset.Nonempty`	`Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.image` `LinearOrder.toDecidableEq` `ConditionallyCompleteLinearOrder.toLinearOrder` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`Finset.ciSup_mem_image` `csSup_empty`
`csInf_eq_min'` 📖	mathematical	`Finset.Nonempty`	`InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.min'` `ConditionallyCompleteLinearOrder.toLinearOrder`	—	`csSup_eq_max'`
`csInf_mem` 📖	mathematical	`Finset.Nonempty`	`Finset` `SetLike.instMembership` `Finset.instSetLike` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `SetLike.coe`	—	`csSup_mem`
`csSup_eq_max'` 📖	mathematical	`Finset.Nonempty`	`SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.max'` `ConditionallyCompleteLinearOrder.toLinearOrder`	—	`eq_of_forall_ge_iff` `csSup_le_iff` `Finset.bddAbove` `supSet_to_nonempty` `to_set` `Finset.max'_le_iff`
`csSup_mem` 📖	mathematical	`Finset.Nonempty`	`Finset` `SetLike.instMembership` `Finset.instSetLike` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `SetLike.coe`	—	`csSup_eq_max'` `Finset.max'_mem`

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iInf_mem_map_of_exists_le_sInf_empty` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `Set` `Set.instEmptyCollection`	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`iInf_congr_Prop` `Finset.ciInf_mem_image`
`iSup_mem_map_of_exists_sSup_empty_le` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `Set` `Set.instEmptyCollection`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`iSup_congr_Prop` `Finset.ciSup_mem_image`
`iSup_mem_map_of_ne_nil` 📖	mathematical	—	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder`	—	`iSup_mem_map_of_exists_sSup_empty_le` `csSup_empty`

Multiset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iInf_mem_map_of_exists_le_sInf_empty` 📖	mathematical	`Multiset` `instMembership` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `Set` `Set.instEmptyCollection`	`Multiset` `instMembership` `map` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`iInf_congr_Prop` `Finset.ciInf_mem_image`
`iSup_mem_map_of_exists_sSup_empty_le` 📖	mathematical	`Multiset` `instMembership` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `Set` `Set.instEmptyCollection`	`Multiset` `instMembership` `map` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`iSup_congr_Prop` `Finset.ciSup_mem_image`
`iSup_mem_map_of_ne_zero` 📖	mathematical	—	`Multiset` `instMembership` `map` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder`	—	`iSup_mem_map_of_exists_sSup_empty_le` `csSup_empty` `exists_mem_of_ne_zero`

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ciInf_mem_image` 📖	mathematical	`Set` `Set.instMembership` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `Set.instEmptyCollection`	`Set` `Set.instMembership` `Set.image` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`CanLift.prf` `Set.instCanLiftFinsetCoeFinite` `iInf_congr_Prop` `Finset.ciInf_mem_image`
`ciSup_lt_iff` 📖	mathematical	`Set` `Set.instMembership` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `Set.instEmptyCollection`	`Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `Set` `Set.instMembership`	—	`LT.lt.trans_le'` `le_csSup` `bddAbove` `SemilatticeSup.instIsDirectedOrder` `supSet_to_nonempty` `subset` `union` `image` `Set.finite_singleton` `ciSup_eq_ite` `Set.union_singleton` `iSup_congr_Prop` `ciSup_unique` `ciSup_mem_image`
`ciSup_mem_image` 📖	mathematical	`Set` `Set.instMembership` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `Set.instEmptyCollection`	`Set` `Set.instMembership` `Set.image` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`CanLift.prf` `Set.instCanLiftFinsetCoeFinite` `iSup_congr_Prop` `Finset.ciSup_mem_image`
`csSup_lt_iff` 📖	mathematical	`Set.Nonempty`	`Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet`	—	`LE.le.trans_lt` `le_csSup` `bddAbove` `SemilatticeSup.instIsDirectedOrder` `supSet_to_nonempty` `Set.Nonempty.csSup_mem`
`lt_ciInf_iff` 📖	mathematical	`Set` `Set.instMembership` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `Set.instEmptyCollection`	`Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `Set` `Set.instMembership`	—	`LT.lt.trans_le` `csInf_le` `bddBelow` `SemilatticeInf.instIsCodirectedOrder` `supSet_to_nonempty` `subset` `union` `image` `Set.finite_singleton` `ciInf_eq_ite` `Set.union_singleton` `iInf_congr_Prop` `ciInf_unique` `ciInf_mem_image`
`lt_csInf_iff` 📖	mathematical	`Set.Nonempty`	`Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf`	—	`csSup_lt_iff`

Set.Nonempty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ciSup_lt_iff` 📖	mathematical	`Set.Nonempty`	`Preorder.toLT` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `Set` `Set.instMembership`	—	`Set.Finite.ciSup_lt_iff` `csSup_empty`
`ciSup_mem_image` 📖	mathematical	`Set.Nonempty`	`Set` `Set.instMembership` `Set.image` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder`	—	`Set.Finite.ciSup_mem_image` `csSup_empty`
`csInf_mem` 📖	mathematical	`Set.Nonempty`	`Set` `Set.instMembership` `InfSet.sInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`csSup_mem`
`csSup_mem` 📖	mathematical	`Set.Nonempty`	`Set` `Set.instMembership` `SupSet.sSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`CanLift.prf` `Set.instCanLiftFinsetCoeFinite` `Finset.Nonempty.csSup_mem`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_eq_ciInf_of_finite` 📖	mathematical	—	`iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`Set.Nonempty.csInf_mem` `Set.range_nonempty` `Set.finite_range`
`exists_eq_ciSup_of_finite` 📖	mathematical	—	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`Set.Nonempty.csSup_mem` `Set.range_nonempty` `Set.finite_range`

---

← Back to Index