Sups

📁 Source: Mathlib/Data/Set/Sups.lean

Statistics

Metric	Count
Definitions `HasInfs`, `infs`, `HasSups`, `sups`, `hasInfs`, `hasSups`, `«term_⊻_»`, `«term_⊼_»`	8
Theorems `infs`, `of_infs_left`, `of_infs_right`, `of_sups_left`, `of_sups_right`, `sups`, `empty_infs`, `empty_sups`, `forall_infs_iff`, `forall_sups_iff`, `iUnion_image_inf_left`, `iUnion_image_inf_right`, `iUnion_image_sup_left`, `iUnion_image_sup_right`, `image_inf_prod`, `image_infs`, `image_subset_infs_left`, `image_subset_infs_right`, `image_subset_sups_left`, `image_subset_sups_right`, `image_sup_prod`, `image_sups`, `inf_mem_infs`, `infs_assoc`, `infs_comm`, `infs_empty`, `infs_eq_empty`, `infs_infs_infs_comm`, `infs_inter_subset_left`, `infs_inter_subset_right`, `infs_left_comm`, `infs_nonempty`, `infs_right_comm`, `infs_self`, `infs_self_subset`, `infs_singleton`, `infs_subset`, `infs_subset_iff`, `infs_subset_left`, `infs_subset_right`, `infs_sups_subset_left`, `infs_sups_subset_right`, `infs_union_left`, `infs_union_right`, `mem_infs`, `mem_sups`, `sep_infs_le`, `sep_sups_le`, `singleton_infs`, `singleton_infs_singleton`, `singleton_sups`, `singleton_sups_singleton`, `subset_infs_self`, `subset_sups_self`, `sup_mem_sups`, `sups_assoc`, `sups_comm`, `sups_empty`, `sups_eq_empty`, `sups_eq_self`, `sups_infs_subset_left`, `sups_infs_subset_right`, `sups_inter_subset_left`, `sups_inter_subset_right`, `sups_left_comm`, `sups_nonempty`, `sups_right_comm`, `sups_singleton`, `sups_subset`, `sups_subset_iff`, `sups_subset_left`, `sups_subset_right`, `sups_subset_self`, `sups_sups_sups_comm`, `sups_union_left`, `sups_union_right`, `lowerClosure_infs`, `upperClosure_sups`	78
Total	86

HasInfs

Definitions

Name	Category	Theorems
`infs` 📖	CompOp	96 math math: `Set.image_subset_infs_left`, `Finset.image_subset_infs_left`, `Finset.univ_infs_univ`, `Finset.infs_nonempty`, `Set.infs_comm`, `Finset.truncatedSup_infs`, `Finset.coe_infs`, `lowerClosure_infs`, `Finset.infs_comm`, `Set.infs_sups_subset_right`, `Set.mem_infs`, `Set.infs_subset_right`, `Set.infs_union_right`, `Set.subset_infs_self`, `Finset.inter_mem_infs`, `Set.infs_infs_infs_comm`, `Set.image_infs`, `AhlswedeZhang.supSum_union_add_supSum_infs`, `Finset.sups_infs_subset_left`, `Set.infs_assoc`, `Set.infs_self_subset`, `Finset.infs_sups_subset_right`, `Finset.powerset_infs_powerset_self`, `Set.infs_singleton`, `Finset.singleton_infs`, `Finset.infs_infs_infs_comm`, `Set.infs_subset_iff`, `Set.sups_infs_subset_left`, `Finset.infs_subset_left`, `Set.infs_subset_left`, `Set.sep_infs_le`, `Set.singleton_infs_singleton`, `Finset.filter_infs_le`, `Finset.diffs_compls_eq_infs`, `Finset.infs_eq_empty`, `Finset.empty_infs`, `Finset.infs_self`, `Finset.card_infs_le`, `Set.Nonempty.infs`, `Finset.infs_left_comm`, `Set.infs_self`, `Finset.sups_infs_subset_right`, `Finset.singleton_infs_singleton`, `Set.infs_sups_subset_left`, `Finset.compls_sups`, `Set.infs_eq_empty`, `Finset.image_infs`, `Finset.image_subset_infs_right`, `Finset.compls_infs`, `Finset.powerset_inter`, `Finset.infs_singleton`, `Finset.biUnion_image_inf_right`, `Set.inf_mem_infs`, `Finset.le_card_infs_mul_card_sups`, `Finset.infs_compls_eq_diffs`, `Finset.infs_union_right`, `Finset.infs_right_comm`, `Finset.compls_infs_eq_diffs`, `Finset.infs_assoc`, `Set.empty_infs`, `Finset.card_infs_iff`, `Finset.infs_empty`, `Set.sups_infs_subset_right`, `Finset.map_infs`, `collapse_modular`, `Set.singleton_infs`, `Finset.mem_infs`, `Finset.Nonempty.infs`, `Finset.infs_sups_subset_left`, `Finset.infs_self_subset`, `Set.image_subset_infs_right`, `Finset.truncatedSup_infs_of_notMem`, `Set.infs_empty`, `Finset.infs_subset`, `Set.infs_nonempty`, `Finset.infs_inter_subset_left`, `Set.infs_subset`, `Set.infs_union_left`, `Finset.biUnion_image_inf_left`, `Set.infs_inter_subset_left`, `Set.infs_right_comm`, `Finset.infs_subset_right`, `Finset.infs_subset_iff`, `Finset.infs_inter_subset_right`, `Finset.inf_mem_infs`, `four_functions_theorem`, `Finset.infs_union_left`, `Set.infs_inter_subset_right`, `Finset.subset_infs_self`, `Set.iUnion_image_inf_left`, `Finset.four_functions_theorem`, `Finset.card_truncatedSup_union_add_card_truncatedSup_infs`, `Set.infs_left_comm`, `Set.iUnion_image_inf_right`, `Set.image_inf_prod`, `Finset.image_inf_product`

HasSups

Definitions

Name	Category	Theorems
`sups` 📖	CompOp	94 math math: `Set.sups_nonempty`, `Set.mem_sups`, `Set.infs_sups_subset_right`, `Set.sups_subset_right`, `Set.sup_mem_sups`, `Set.singleton_sups_singleton`, `Set.subset_sups_self`, `upperClosure_sups`, `Set.sups_assoc`, `Finset.sups_inter_subset_right`, `Set.sups_subset_left`, `Set.sups_right_comm`, `Finset.powerset_sups_powerset_self`, `Set.sups_union_left`, `Finset.card_sups_iff`, `Finset.sups_infs_subset_left`, `Finset.univ_sups_univ`, `Finset.singleton_sups_singleton`, `Finset.image_subset_sups_left`, `Finset.infs_sups_subset_right`, `Finset.sups_singleton`, `Finset.sups_assoc`, `Set.sups_comm`, `Set.sups_inter_subset_right`, `Set.image_subset_sups_right`, `Set.sups_left_comm`, `Set.Nonempty.sups`, `Finset.sups_subset_right`, `Finset.image_subset_sups_right`, `Set.sups_infs_subset_left`, `Finset.sups_eq_empty`, `Finset.sups_empty`, `Set.sep_sups_le`, `Finset.coe_sups`, `Finset.sups_union_right`, `Finset.union_mem_sups`, `Set.iUnion_image_sup_right`, `Finset.sups_right_comm`, `Set.sups_union_right`, `Finset.sup_mem_sups`, `Finset.empty_sups`, `Finset.sups_union_left`, `Finset.sups_left_comm`, `Finset.card_truncatedInf_union_add_card_truncatedInf_sups`, `Finset.truncatedInf_sups_of_notMem`, `Finset.sups_infs_subset_right`, `Finset.sups_subset_self`, `Set.infs_sups_subset_left`, `Finset.compls_sups`, `Finset.sups_nonempty`, `Set.singleton_sups`, `Finset.biUnion_image_sup_right`, `Finset.compls_infs`, `Finset.filter_sups_le`, `Finset.image_sup_product`, `Set.sups_sups_sups_comm`, `Finset.sups_subset_left`, `Finset.le_card_infs_mul_card_sups`, `Finset.biUnion_image_sup_left`, `Set.sups_singleton`, `Finset.sups_comm`, `Finset.map_sups`, `Set.sups_inter_subset_left`, `Finset.card_sups_le`, `Set.image_sups`, `Finset.sups_sups_sups_comm`, `Set.sups_eq_self`, `Finset.sups_subset_iff`, `Set.empty_sups`, `Finset.truncatedInf_sups`, `Set.sups_infs_subset_right`, `Finset.subset_sups_self`, `Finset.sups_eq_self`, `collapse_modular`, `Set.sups_subset`, `Finset.singleton_sups`, `Finset.sups_subset`, `Finset.Nonempty.sups`, `Finset.image_sups`, `Set.image_sup_prod`, `Finset.powerset_union`, `Finset.disjSups_subset_sups`, `Finset.infs_sups_subset_left`, `Set.sups_subset_self`, `Finset.sups_inter_subset_left`, `Set.sups_empty`, `Set.sups_eq_empty`, `Finset.mem_sups`, `four_functions_theorem`, `AhlswedeZhang.infSum_union_add_infSum_sups`, `Set.sups_subset_iff`, `Set.image_subset_sups_left`, `Finset.four_functions_theorem`, `Set.iUnion_image_sup_left`

Set

Definitions

Name	Category	Theorems
`hasInfs` 📖	CompOp	39 math math: `image_subset_infs_left`, `infs_comm`, `Finset.coe_infs`, `lowerClosure_infs`, `infs_sups_subset_right`, `mem_infs`, `infs_subset_right`, `infs_union_right`, `subset_infs_self`, `infs_infs_infs_comm`, `image_infs`, `infs_assoc`, `infs_self_subset`, `infs_singleton`, `infs_subset_iff`, `sups_infs_subset_left`, `infs_subset_left`, `sep_infs_le`, `singleton_infs_singleton`, `Nonempty.infs`, `infs_self`, `infs_sups_subset_left`, `infs_eq_empty`, `inf_mem_infs`, `empty_infs`, `sups_infs_subset_right`, `singleton_infs`, `image_subset_infs_right`, `infs_empty`, `infs_nonempty`, `infs_subset`, `infs_union_left`, `infs_inter_subset_left`, `infs_right_comm`, `infs_inter_subset_right`, `iUnion_image_inf_left`, `infs_left_comm`, `iUnion_image_inf_right`, `image_inf_prod`
`hasSups` 📖	CompOp	39 math math: `sups_nonempty`, `mem_sups`, `infs_sups_subset_right`, `sups_subset_right`, `sup_mem_sups`, `singleton_sups_singleton`, `subset_sups_self`, `upperClosure_sups`, `sups_assoc`, `sups_subset_left`, `sups_right_comm`, `sups_union_left`, `sups_comm`, `sups_inter_subset_right`, `image_subset_sups_right`, `sups_left_comm`, `Nonempty.sups`, `sups_infs_subset_left`, `sep_sups_le`, `Finset.coe_sups`, `iUnion_image_sup_right`, `sups_union_right`, `infs_sups_subset_left`, `singleton_sups`, `sups_sups_sups_comm`, `sups_singleton`, `sups_inter_subset_left`, `image_sups`, `sups_eq_self`, `empty_sups`, `sups_infs_subset_right`, `sups_subset`, `image_sup_prod`, `sups_subset_self`, `sups_empty`, `sups_eq_empty`, `sups_subset_iff`, `image_subset_sups_left`, `iUnion_image_sup_left`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`empty_infs` 📖	mathematical	—	`HasInfs.infs` `Set` `hasInfs` `instEmptyCollection`	—	`image2_empty_left`
`empty_sups` 📖	mathematical	—	`HasSups.sups` `Set` `hasSups` `instEmptyCollection`	—	`image2_empty_left`
`forall_infs_iff` 📖	mathematical	—	`SemilatticeInf.toMin`	—	`forall_mem_image2`
`forall_sups_iff` 📖	mathematical	—	`SemilatticeSup.toMax`	—	`forall_mem_image2`
`iUnion_image_inf_left` 📖	mathematical	—	`iUnion` `Set` `instMembership` `image` `SemilatticeInf.toMin` `HasInfs.infs` `hasInfs`	—	`iUnion_image_left`
`iUnion_image_inf_right` 📖	mathematical	—	`iUnion` `Set` `instMembership` `image` `SemilatticeInf.toMin` `HasInfs.infs` `hasInfs`	—	`iUnion_image_right`
`iUnion_image_sup_left` 📖	mathematical	—	`iUnion` `Set` `instMembership` `image` `HasSups.sups` `hasSups`	—	`iUnion_image_left`
`iUnion_image_sup_right` 📖	mathematical	—	`iUnion` `Set` `instMembership` `image` `SemilatticeSup.toMax` `HasSups.sups` `hasSups`	—	`iUnion_image_right`
`image_inf_prod` 📖	mathematical	—	`image2` `SemilatticeInf.toMin` `HasInfs.infs` `Set` `hasInfs`	—	—
`image_infs` 📖	mathematical	—	`image` `DFunLike.coe` `HasInfs.infs` `Set` `hasInfs`	—	`image_image2_distrib` `InfHomClass.map_inf`
`image_subset_infs_left` 📖	mathematical	`Set` `instMembership`	`instHasSubset` `image` `SemilatticeInf.toMin` `HasInfs.infs` `hasInfs`	—	`image_subset_image2_left`
`image_subset_infs_right` 📖	mathematical	`Set` `instMembership`	`instHasSubset` `image` `SemilatticeInf.toMin` `HasInfs.infs` `hasInfs`	—	`image_subset_image2_right`
`image_subset_sups_left` 📖	mathematical	`Set` `instMembership`	`instHasSubset` `image` `SemilatticeSup.toMax` `HasSups.sups` `hasSups`	—	`image_subset_image2_left`
`image_subset_sups_right` 📖	mathematical	`Set` `instMembership`	`instHasSubset` `image` `HasSups.sups` `hasSups`	—	`image_subset_image2_right`
`image_sup_prod` 📖	mathematical	—	`image2` `SemilatticeSup.toMax` `HasSups.sups` `Set` `hasSups`	—	—
`image_sups` 📖	mathematical	—	`image` `DFunLike.coe` `HasSups.sups` `Set` `hasSups`	—	`image_image2_distrib` `SupHomClass.map_sup`
`inf_mem_infs` 📖	mathematical	`Set` `instMembership`	`HasInfs.infs` `hasInfs` `SemilatticeInf.toMin`	—	`mem_image2_of_mem`
`infs_assoc` 📖	mathematical	—	`HasInfs.infs` `Set` `hasInfs`	—	`image2_assoc` `inf_assoc`
`infs_comm` 📖	mathematical	—	`HasInfs.infs` `Set` `hasInfs`	—	`image2_comm` `inf_comm`
`infs_empty` 📖	mathematical	—	`HasInfs.infs` `Set` `hasInfs` `instEmptyCollection`	—	`image2_empty_right`
`infs_eq_empty` 📖	mathematical	—	`HasInfs.infs` `Set` `hasInfs` `instEmptyCollection`	—	`image2_eq_empty_iff`
`infs_infs_infs_comm` 📖	mathematical	—	`HasInfs.infs` `Set` `hasInfs`	—	`image2_image2_image2_comm` `inf_inf_inf_comm`
`infs_inter_subset_left` 📖	mathematical	—	`Set` `instHasSubset` `HasInfs.infs` `hasInfs` `instInter`	—	`image2_inter_subset_left`
`infs_inter_subset_right` 📖	mathematical	—	`Set` `instHasSubset` `HasInfs.infs` `hasInfs` `instInter`	—	`image2_inter_subset_right`
`infs_left_comm` 📖	mathematical	—	`HasInfs.infs` `Set` `hasInfs`	—	`image2_left_comm` `inf_left_comm`
`infs_nonempty` 📖	mathematical	—	`Nonempty` `HasInfs.infs` `Set` `hasInfs`	—	`image2_nonempty_iff`
`infs_right_comm` 📖	mathematical	—	`HasInfs.infs` `Set` `hasInfs`	—	`image2_right_comm` `inf_right_comm`
`infs_self` 📖	mathematical	—	`HasInfs.infs` `Set` `hasInfs` `InfClosed`	—	`LE.le.ge_iff_eq'` `HasSubset.Subset.le` `subset_infs_self` `infs_self_subset`
`infs_self_subset` 📖	mathematical	—	`Set` `instHasSubset` `HasInfs.infs` `hasInfs` `InfClosed`	—	`infs_subset_iff`
`infs_singleton` 📖	mathematical	—	`HasInfs.infs` `Set` `hasInfs` `instSingletonSet` `image` `SemilatticeInf.toMin`	—	`image2_singleton_right`
`infs_subset` 📖	mathematical	`Set` `instHasSubset`	`HasInfs.infs` `hasInfs`	—	`image2_subset`
`infs_subset_iff` 📖	mathematical	—	`Set` `instHasSubset` `HasInfs.infs` `hasInfs` `instMembership` `SemilatticeInf.toMin`	—	`image2_subset_iff`
`infs_subset_left` 📖	mathematical	`Set` `instHasSubset`	`HasInfs.infs` `hasInfs`	—	`image2_subset_left`
`infs_subset_right` 📖	mathematical	`Set` `instHasSubset`	`HasInfs.infs` `hasInfs`	—	`image2_subset_right`
`infs_sups_subset_left` 📖	mathematical	—	`Set` `instHasSubset` `HasInfs.infs` `hasInfs` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `HasSups.sups` `hasSups` `Lattice.toSemilatticeSup`	—	`image2_distrib_subset_left` `inf_sup_left`
`infs_sups_subset_right` 📖	mathematical	—	`Set` `instHasSubset` `HasInfs.infs` `hasInfs` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `HasSups.sups` `hasSups` `Lattice.toSemilatticeSup`	—	`image2_distrib_subset_right` `inf_sup_right`
`infs_union_left` 📖	mathematical	—	`HasInfs.infs` `Set` `hasInfs` `instUnion`	—	`image2_union_left`
`infs_union_right` 📖	mathematical	—	`HasInfs.infs` `Set` `hasInfs` `instUnion`	—	`image2_union_right`
`mem_infs` 📖	mathematical	—	`Set` `instMembership` `HasInfs.infs` `hasInfs` `SemilatticeInf.toMin`	—	—
`mem_sups` 📖	mathematical	—	`Set` `instMembership` `HasSups.sups` `hasSups` `SemilatticeSup.toMax`	—	—
`sep_infs_le` 📖	mathematical	—	`setOf` `Set` `instMembership` `HasInfs.infs` `hasInfs` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder`	—	`ext`
`sep_sups_le` 📖	mathematical	—	`setOf` `Set` `instMembership` `HasSups.sups` `hasSups` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	—	`ext`
`singleton_infs` 📖	mathematical	—	`HasInfs.infs` `Set` `hasInfs` `instSingletonSet` `image` `SemilatticeInf.toMin`	—	`image2_singleton_left`
`singleton_infs_singleton` 📖	mathematical	—	`HasInfs.infs` `Set` `hasInfs` `instSingletonSet` `SemilatticeInf.toMin`	—	`image2_singleton`
`singleton_sups` 📖	mathematical	—	`HasSups.sups` `Set` `hasSups` `instSingletonSet` `image` `SemilatticeSup.toMax`	—	`image2_singleton_left`
`singleton_sups_singleton` 📖	mathematical	—	`HasSups.sups` `Set` `hasSups` `instSingletonSet` `SemilatticeSup.toMax`	—	`image2_singleton`
`subset_infs_self` 📖	mathematical	—	`Set` `instHasSubset` `HasInfs.infs` `hasInfs`	—	`mem_infs` `inf_idem`
`subset_sups_self` 📖	mathematical	—	`Set` `instHasSubset` `HasSups.sups` `hasSups`	—	`mem_sups` `sup_idem`
`sup_mem_sups` 📖	mathematical	`Set` `instMembership`	`HasSups.sups` `hasSups` `SemilatticeSup.toMax`	—	`mem_image2_of_mem`
`sups_assoc` 📖	mathematical	—	`HasSups.sups` `Set` `hasSups`	—	`image2_assoc` `sup_assoc`
`sups_comm` 📖	mathematical	—	`HasSups.sups` `Set` `hasSups`	—	`image2_comm` `sup_comm`
`sups_empty` 📖	mathematical	—	`HasSups.sups` `Set` `hasSups` `instEmptyCollection`	—	`image2_empty_right`
`sups_eq_empty` 📖	mathematical	—	`HasSups.sups` `Set` `hasSups` `instEmptyCollection`	—	`image2_eq_empty_iff`
`sups_eq_self` 📖	mathematical	—	`HasSups.sups` `Set` `hasSups` `SupClosed`	—	`LE.le.ge_iff_eq'` `HasSubset.Subset.le` `subset_sups_self` `sups_subset_self`
`sups_infs_subset_left` 📖	mathematical	—	`Set` `instHasSubset` `HasSups.sups` `hasSups` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `HasInfs.infs` `hasInfs` `Lattice.toSemilatticeInf`	—	`image2_distrib_subset_left` `sup_inf_left`
`sups_infs_subset_right` 📖	mathematical	—	`Set` `instHasSubset` `HasSups.sups` `hasSups` `Lattice.toSemilatticeSup` `DistribLattice.toLattice` `HasInfs.infs` `hasInfs` `Lattice.toSemilatticeInf`	—	`image2_distrib_subset_right` `sup_inf_right`
`sups_inter_subset_left` 📖	mathematical	—	`Set` `instHasSubset` `HasSups.sups` `hasSups` `instInter`	—	`image2_inter_subset_left`
`sups_inter_subset_right` 📖	mathematical	—	`Set` `instHasSubset` `HasSups.sups` `hasSups` `instInter`	—	`image2_inter_subset_right`
`sups_left_comm` 📖	mathematical	—	`HasSups.sups` `Set` `hasSups`	—	`image2_left_comm` `sup_left_comm`
`sups_nonempty` 📖	mathematical	—	`Nonempty` `HasSups.sups` `Set` `hasSups`	—	`image2_nonempty_iff`
`sups_right_comm` 📖	mathematical	—	`HasSups.sups` `Set` `hasSups`	—	`image2_right_comm` `sup_right_comm`
`sups_singleton` 📖	mathematical	—	`HasSups.sups` `Set` `hasSups` `instSingletonSet` `image` `SemilatticeSup.toMax`	—	`image2_singleton_right`
`sups_subset` 📖	mathematical	`Set` `instHasSubset`	`HasSups.sups` `hasSups`	—	`image2_subset`
`sups_subset_iff` 📖	mathematical	—	`Set` `instHasSubset` `HasSups.sups` `hasSups` `instMembership` `SemilatticeSup.toMax`	—	`image2_subset_iff`
`sups_subset_left` 📖	mathematical	`Set` `instHasSubset`	`HasSups.sups` `hasSups`	—	`image2_subset_left`
`sups_subset_right` 📖	mathematical	`Set` `instHasSubset`	`HasSups.sups` `hasSups`	—	`image2_subset_right`
`sups_subset_self` 📖	mathematical	—	`Set` `instHasSubset` `HasSups.sups` `hasSups` `SupClosed`	—	`sups_subset_iff`
`sups_sups_sups_comm` 📖	mathematical	—	`HasSups.sups` `Set` `hasSups`	—	`image2_image2_image2_comm` `sup_sup_sup_comm`
`sups_union_left` 📖	mathematical	—	`HasSups.sups` `Set` `hasSups` `instUnion`	—	`image2_union_left`
`sups_union_right` 📖	mathematical	—	`HasSups.sups` `Set` `hasSups` `instUnion`	—	`image2_union_right`

Set.Nonempty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`infs` 📖	mathematical	`Set.Nonempty`	`HasInfs.infs` `Set` `Set.hasInfs`	—	`image2`
`of_infs_left` 📖	—	`Set.Nonempty` `HasInfs.infs` `Set` `Set.hasInfs`	—	—	`of_image2_left`
`of_infs_right` 📖	—	`Set.Nonempty` `HasInfs.infs` `Set` `Set.hasInfs`	—	—	`of_image2_right`
`of_sups_left` 📖	—	`Set.Nonempty` `HasSups.sups` `Set` `Set.hasSups`	—	—	`of_image2_left`
`of_sups_right` 📖	—	`Set.Nonempty` `HasSups.sups` `Set` `Set.hasSups`	—	—	`of_image2_right`
`sups` 📖	mathematical	`Set.Nonempty`	`HasSups.sups` `Set` `Set.hasSups`	—	`image2`

(root)

Definitions

Name	Category	Theorems
`HasInfs` 📖	CompData	—
`HasSups` 📖	CompData	—
`«term_⊻_»` 📖	CompOp	—
`«term_⊼_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lowerClosure_infs` 📖	mathematical	—	`lowerClosure` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `HasInfs.infs` `Set` `Set.hasInfs` `LowerSet` `Preorder.toLE` `LowerSet.instMin`	—	`LowerSet.ext` `Set.ext` `LE.le.trans` `inf_le_left` `inf_le_right` `le_inf`
`upperClosure_sups` 📖	mathematical	—	`upperClosure` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `HasSups.sups` `Set` `Set.hasSups` `UpperSet` `Preorder.toLE` `UpperSet.instMax`	—	`UpperSet.ext` `Set.ext` `LE.le.trans` `le_sup_left` `le_sup_right` `sup_le`

---

← Back to Index