Documentation Verification Report

BddLat

📁 Source: Mathlib/Order/Category/BddLat.lean

Statistics

Metric	Count
Definitions `BddLat`, `hom`, `hom`, `hom'`, `mk`, `dual`, `dualEquiv`, `hasForgetToBddOrd`, `hasForgetToLat`, `hasForgetToSemilatInf`, `hasForgetToSemilatSup`, `instCoeSortType`, `instConcreteCategoryBoundedLatticeHomCarrier`, `instInhabited`, `instLargeCategory`, `isBoundedOrder`, `of`, `ofHom`, `toLat`, `latToBddLat`, `latToBddLatCompDualIsoDualCompLatToBddLat`, `latToBddLatForgetAdjunction`	22
Theorems `ext`, `ext_iff`, `mk_hom`, `mk_inv`, `coe_forget_to_bddOrd`, `coe_forget_to_lat`, `coe_forget_to_semilatInf`, `coe_forget_to_semilatSup`, `coe_of`, `comp_apply`, `dualEquiv_functor`, `dualEquiv_inverse`, `dual_map`, `ext`, `ext_iff`, `forget_lat_partOrd_eq_forget_bddOrd_partOrd`, `forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd`, `forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd`, `hom_comp`, `hom_ext`, `hom_ext_iff`, `hom_id`, `id_apply`, `bddLat_dual_comp_forget_to_bddOrd`, `bddLat_dual_comp_forget_to_lat`, `bddLat_dual_comp_forget_to_semilatInfCat`, `bddLat_dual_comp_forget_to_semilatSupCat`	27
Total	49

BddLat

Definitions

Name	Category	Theorems
`dual` 📖	CompOp	8 math math: `bddLat_dual_comp_forget_to_lat`, `bddLat_dual_comp_forget_to_semilatSupCat`, `bddLat_dual_comp_forget_to_semilatInfCat`, `bddLat_dual_comp_forget_to_bddOrd`, `completeLat_dual_comp_forget_to_bddLat`, `dualEquiv_inverse`, `dual_map`, `dualEquiv_functor`
`dualEquiv` 📖	CompOp	2 math math: `dualEquiv_inverse`, `dualEquiv_functor`
`hasForgetToBddOrd` 📖	CompOp	5 math math: `forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd`, `forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd`, `bddLat_dual_comp_forget_to_bddOrd`, `forget_lat_partOrd_eq_forget_bddOrd_partOrd`, `coe_forget_to_bddOrd`
`hasForgetToLat` 📖	CompOp	4 math math: `bddLat_dual_comp_forget_to_lat`, `forget_lat_partOrd_eq_forget_bddOrd_partOrd`, `coe_forget_to_lat`, `BddDistLat.forget_bddLat_lat_eq_forget_distLat_lat`
`hasForgetToSemilatInf` 📖	CompOp	4 math math: `forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd`, `bddLat_dual_comp_forget_to_semilatSupCat`, `bddLat_dual_comp_forget_to_semilatInfCat`, `coe_forget_to_semilatInf`
`hasForgetToSemilatSup` 📖	CompOp	4 math math: `forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd`, `bddLat_dual_comp_forget_to_semilatSupCat`, `bddLat_dual_comp_forget_to_semilatInfCat`, `coe_forget_to_semilatSup`
`instCoeSortType` 📖	CompOp	—
`instConcreteCategoryBoundedLatticeHomCarrier` 📖	CompOp	14 math math: `bddLat_dual_comp_forget_to_lat`, `forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd`, `forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd`, `bddLat_dual_comp_forget_to_semilatSupCat`, `bddLat_dual_comp_forget_to_semilatInfCat`, `bddLat_dual_comp_forget_to_bddOrd`, `forget_lat_partOrd_eq_forget_bddOrd_partOrd`, `coe_forget_to_lat`, `BddDistLat.forget_bddLat_lat_eq_forget_distLat_lat`, `completeLat_dual_comp_forget_to_bddLat`, `coe_forget_to_semilatSup`, `coe_forget_to_bddOrd`, `coe_forget_to_semilatInf`, `ext_iff`
`instInhabited` 📖	CompOp	—
`instLargeCategory` 📖	CompOp	19 math math: `bddLat_dual_comp_forget_to_lat`, `forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd`, `forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd`, `bddLat_dual_comp_forget_to_semilatSupCat`, `bddLat_dual_comp_forget_to_semilatInfCat`, `bddLat_dual_comp_forget_to_bddOrd`, `forget_lat_partOrd_eq_forget_bddOrd_partOrd`, `coe_forget_to_lat`, `BddDistLat.forget_bddLat_lat_eq_forget_distLat_lat`, `Iso.mk_hom`, `completeLat_dual_comp_forget_to_bddLat`, `coe_forget_to_semilatSup`, `dualEquiv_inverse`, `coe_forget_to_bddOrd`, `coe_forget_to_semilatInf`, `ext_iff`, `dual_map`, `dualEquiv_functor`, `Iso.mk_inv`
`isBoundedOrder` 📖	CompOp	17 math math: `bddLat_dual_comp_forget_to_lat`, `forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd`, `forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd`, `bddLat_dual_comp_forget_to_semilatSupCat`, `bddLat_dual_comp_forget_to_semilatInfCat`, `bddLat_dual_comp_forget_to_bddOrd`, `forget_lat_partOrd_eq_forget_bddOrd_partOrd`, `coe_forget_to_lat`, `BddDistLat.forget_bddLat_lat_eq_forget_distLat_lat`, `Iso.mk_hom`, `completeLat_dual_comp_forget_to_bddLat`, `coe_forget_to_semilatSup`, `coe_forget_to_bddOrd`, `coe_forget_to_semilatInf`, `ext_iff`, `dual_map`, `Iso.mk_inv`
`of` 📖	CompOp	1 math math: `coe_of`
`ofHom` 📖	CompOp	3 math math: `Iso.mk_hom`, `dual_map`, `Iso.mk_inv`
`toLat` 📖	CompOp	17 math math: `bddLat_dual_comp_forget_to_lat`, `forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd`, `BddDistLat.coe_toBddLat`, `forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd`, `coe_of`, `bddLat_dual_comp_forget_to_semilatSupCat`, `bddLat_dual_comp_forget_to_semilatInfCat`, `bddLat_dual_comp_forget_to_bddOrd`, `forget_lat_partOrd_eq_forget_bddOrd_partOrd`, `coe_forget_to_lat`, `BddDistLat.forget_bddLat_lat_eq_forget_distLat_lat`, `completeLat_dual_comp_forget_to_bddLat`, `coe_forget_to_semilatSup`, `coe_forget_to_bddOrd`, `coe_forget_to_semilatInf`, `ext_iff`, `dual_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_forget_to_bddOrd` 📖	mathematical	—	`PartOrd.carrier` `BddOrd.toPartOrd` `CategoryTheory.Functor.obj` `BddLat` `instLargeCategory` `BddOrd` `BddOrd.instCategory` `CategoryTheory.forget₂` `BoundedLatticeHom` `Lat.carrier` `toLat` `Lat.str` `isBoundedOrder` `BoundedLatticeHom.instFunLike` `instConcreteCategoryBoundedLatticeHomCarrier` `BoundedOrderHom` `PartialOrder.toPreorder` `PartOrd.str` `BddOrd.isBoundedOrder` `BoundedOrderHom.instFunLike` `BddOrd.instConcreteCategoryBoundedOrderHomCarrier` `hasForgetToBddOrd`	—	—
`coe_forget_to_lat` 📖	mathematical	—	`Lat.carrier` `CategoryTheory.Functor.obj` `BddLat` `instLargeCategory` `Lat` `Lat.instCategory` `CategoryTheory.forget₂` `BoundedLatticeHom` `toLat` `Lat.str` `isBoundedOrder` `BoundedLatticeHom.instFunLike` `instConcreteCategoryBoundedLatticeHomCarrier` `LatticeHom` `LatticeHom.instFunLike` `Lat.instConcreteCategoryLatticeHomCarrier` `hasForgetToLat`	—	—
`coe_forget_to_semilatInf` 📖	mathematical	—	`SemilatInfCat.X` `CategoryTheory.Functor.obj` `BddLat` `instLargeCategory` `SemilatInfCat` `SemilatInfCat.instLargeCategory` `CategoryTheory.forget₂` `BoundedLatticeHom` `Lat.carrier` `toLat` `Lat.str` `isBoundedOrder` `BoundedLatticeHom.instFunLike` `instConcreteCategoryBoundedLatticeHomCarrier` `InfTopHom` `SemilatticeInf.toMin` `SemilatInfCat.isSemilatticeInf` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SemilatInfCat.isOrderTop` `InfTopHom.instFunLike` `SemilatInfCat.instConcreteCategoryInfTopHomX` `hasForgetToSemilatInf`	—	—
`coe_forget_to_semilatSup` 📖	mathematical	—	`SemilatSupCat.X` `CategoryTheory.Functor.obj` `BddLat` `instLargeCategory` `SemilatSupCat` `SemilatSupCat.instLargeCategory` `CategoryTheory.forget₂` `BoundedLatticeHom` `Lat.carrier` `toLat` `Lat.str` `isBoundedOrder` `BoundedLatticeHom.instFunLike` `instConcreteCategoryBoundedLatticeHomCarrier` `SupBotHom` `SemilatticeSup.toMax` `SemilatSupCat.isSemilatticeSup` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SemilatSupCat.isOrderBot` `SupBotHom.instFunLike` `SemilatSupCat.instConcreteCategorySupBotHomX` `hasForgetToSemilatSup`	—	—
`coe_of` 📖	mathematical	—	`Lat.carrier` `toLat` `of`	—	—
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `Lat.carrier` `CategoryTheory.ConcreteCategory.hom` `Lat` `Lat.instCategory` `LatticeHom` `Lat.str` `LatticeHom.instFunLike` `Lat.instConcreteCategoryLatticeHomCarrier` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	—
`dualEquiv_functor` 📖	mathematical	—	`CategoryTheory.Equivalence.functor` `BddLat` `instLargeCategory` `dualEquiv` `dual`	—	—
`dualEquiv_inverse` 📖	mathematical	—	`CategoryTheory.Equivalence.inverse` `BddLat` `instLargeCategory` `dualEquiv` `dual`	—	—
`dual_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `BddLat` `instLargeCategory` `dual` `ofHom` `OrderDual` `Lat.carrier` `toLat` `OrderDual.instLattice` `Lat.str` `OrderDual.instBoundedOrder` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `isBoundedOrder` `DFunLike.coe` `Equiv` `BoundedLatticeHom` `EquivLike.toFunLike` `Equiv.instEquivLike` `BoundedLatticeHom.dual` `Hom.hom`	—	—
`ext` 📖	—	`DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `BddLat` `instLargeCategory` `BoundedLatticeHom` `Lat.carrier` `toLat` `Lat.str` `isBoundedOrder` `BoundedLatticeHom.instFunLike` `instConcreteCategoryBoundedLatticeHomCarrier`	—	—	`CategoryTheory.ConcreteCategory.hom_ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `BddLat` `instLargeCategory` `BoundedLatticeHom` `Lat.carrier` `toLat` `Lat.str` `isBoundedOrder` `BoundedLatticeHom.instFunLike` `instConcreteCategoryBoundedLatticeHomCarrier`	—	`ext`
`forget_lat_partOrd_eq_forget_bddOrd_partOrd` 📖	mathematical	—	`CategoryTheory.Functor.comp` `BddLat` `instLargeCategory` `Lat` `Lat.instCategory` `PartOrd` `PartOrd.instCategory` `CategoryTheory.forget₂` `BoundedLatticeHom` `Lat.carrier` `toLat` `Lat.str` `isBoundedOrder` `BoundedLatticeHom.instFunLike` `instConcreteCategoryBoundedLatticeHomCarrier` `LatticeHom` `LatticeHom.instFunLike` `Lat.instConcreteCategoryLatticeHomCarrier` `hasForgetToLat` `OrderHom` `PartOrd.carrier` `PartialOrder.toPreorder` `PartOrd.str` `OrderHom.instFunLike` `PartOrd.instConcreteCategoryOrderHomCarrier` `Lat.hasForgetToPartOrd` `BddOrd` `BddOrd.instCategory` `BoundedOrderHom` `BddOrd.toPartOrd` `BddOrd.isBoundedOrder` `BoundedOrderHom.instFunLike` `BddOrd.instConcreteCategoryBoundedOrderHomCarrier` `hasForgetToBddOrd` `BddOrd.hasForgetToPartOrd`	—	—
`forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd` 📖	mathematical	—	`CategoryTheory.Functor.comp` `BddLat` `instLargeCategory` `SemilatInfCat` `SemilatInfCat.instLargeCategory` `PartOrd` `PartOrd.instCategory` `CategoryTheory.forget₂` `BoundedLatticeHom` `Lat.carrier` `toLat` `Lat.str` `isBoundedOrder` `BoundedLatticeHom.instFunLike` `instConcreteCategoryBoundedLatticeHomCarrier` `InfTopHom` `SemilatInfCat.X` `SemilatticeInf.toMin` `SemilatInfCat.isSemilatticeInf` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SemilatInfCat.isOrderTop` `InfTopHom.instFunLike` `SemilatInfCat.instConcreteCategoryInfTopHomX` `hasForgetToSemilatInf` `OrderHom` `PartOrd.carrier` `PartOrd.str` `OrderHom.instFunLike` `PartOrd.instConcreteCategoryOrderHomCarrier` `SemilatInfCat.hasForgetToPartOrd` `BddOrd` `BddOrd.instCategory` `BoundedOrderHom` `BddOrd.toPartOrd` `BddOrd.isBoundedOrder` `BoundedOrderHom.instFunLike` `BddOrd.instConcreteCategoryBoundedOrderHomCarrier` `hasForgetToBddOrd` `BddOrd.hasForgetToPartOrd`	—	—
`forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd` 📖	mathematical	—	`CategoryTheory.Functor.comp` `BddLat` `instLargeCategory` `SemilatSupCat` `SemilatSupCat.instLargeCategory` `PartOrd` `PartOrd.instCategory` `CategoryTheory.forget₂` `BoundedLatticeHom` `Lat.carrier` `toLat` `Lat.str` `isBoundedOrder` `BoundedLatticeHom.instFunLike` `instConcreteCategoryBoundedLatticeHomCarrier` `SupBotHom` `SemilatSupCat.X` `SemilatticeSup.toMax` `SemilatSupCat.isSemilatticeSup` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SemilatSupCat.isOrderBot` `SupBotHom.instFunLike` `SemilatSupCat.instConcreteCategorySupBotHomX` `hasForgetToSemilatSup` `OrderHom` `PartOrd.carrier` `PartOrd.str` `OrderHom.instFunLike` `PartOrd.instConcreteCategoryOrderHomCarrier` `SemilatSupCat.hasForgetToPartOrd` `BddOrd` `BddOrd.instCategory` `BoundedOrderHom` `BddOrd.toPartOrd` `BddOrd.isBoundedOrder` `BoundedOrderHom.instFunLike` `BddOrd.instConcreteCategoryBoundedOrderHomCarrier` `hasForgetToBddOrd` `BddOrd.hasForgetToPartOrd`	—	—
`hom_comp` 📖	mathematical	—	`Lat.Hom.hom` `CategoryTheory.CategoryStruct.comp` `Lat` `CategoryTheory.Category.toCategoryStruct` `Lat.instCategory` `LatticeHom.comp` `Lat.carrier` `Lat.str`	—	—
`hom_ext` 📖	—	`Hom.hom`	—	—	`Hom.ext`
`hom_ext_iff` 📖	mathematical	—	`Hom.hom`	—	`hom_ext`
`hom_id` 📖	mathematical	—	`Lat.Hom.hom` `CategoryTheory.CategoryStruct.id` `Lat` `CategoryTheory.Category.toCategoryStruct` `Lat.instCategory` `LatticeHom.id` `Lat.carrier` `Lat.str`	—	—
`id_apply` 📖	mathematical	—	`DFunLike.coe` `Lat.carrier` `CategoryTheory.ConcreteCategory.hom` `Lat` `Lat.instCategory` `LatticeHom` `Lat.str` `LatticeHom.instFunLike` `Lat.instConcreteCategoryLatticeHomCarrier` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	—

BddLat.Hom

Definitions

Name	Category	Theorems
`hom` 📖	CompOp	2 math math: `BddLat.hom_ext_iff`, `BddLat.dual_map`
`hom'` 📖	CompOp	1 math math: `ext_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`hom'`	—	—	—
`ext_iff` 📖	mathematical	—	`hom'`	—	`ext`

BddLat.Hom.Simps

Definitions

Name	Category	Theorems
`hom` 📖	CompOp	—

BddLat.Iso

Definitions

Name	Category	Theorems
`mk` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `BddLat` `BddLat.instLargeCategory` `BddLat.ofHom` `Lat.carrier` `Lat.str` `BddLat.isBoundedOrder`	—	—
`mk_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `BddLat` `BddLat.instLargeCategory` `BddLat.ofHom` `Lat.carrier` `Lat.str` `BddLat.isBoundedOrder`	—	—

(root)

Definitions

Name	Category	Theorems
`BddLat` 📖	CompData	19 math math: `bddLat_dual_comp_forget_to_lat`, `BddLat.forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd`, `BddLat.forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd`, `bddLat_dual_comp_forget_to_semilatSupCat`, `bddLat_dual_comp_forget_to_semilatInfCat`, `bddLat_dual_comp_forget_to_bddOrd`, `BddLat.forget_lat_partOrd_eq_forget_bddOrd_partOrd`, `BddLat.coe_forget_to_lat`, `BddDistLat.forget_bddLat_lat_eq_forget_distLat_lat`, `BddLat.Iso.mk_hom`, `completeLat_dual_comp_forget_to_bddLat`, `BddLat.coe_forget_to_semilatSup`, `BddLat.dualEquiv_inverse`, `BddLat.coe_forget_to_bddOrd`, `BddLat.coe_forget_to_semilatInf`, `BddLat.ext_iff`, `BddLat.dual_map`, `BddLat.dualEquiv_functor`, `BddLat.Iso.mk_inv`
`latToBddLat` 📖	CompOp	—
`latToBddLatCompDualIsoDualCompLatToBddLat` 📖	CompOp	—
`latToBddLatForgetAdjunction` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bddLat_dual_comp_forget_to_bddOrd` 📖	mathematical	—	`CategoryTheory.Functor.comp` `BddLat` `BddLat.instLargeCategory` `BddOrd` `BddOrd.instCategory` `BddLat.dual` `CategoryTheory.forget₂` `BoundedLatticeHom` `Lat.carrier` `BddLat.toLat` `Lat.str` `BddLat.isBoundedOrder` `BoundedLatticeHom.instFunLike` `BddLat.instConcreteCategoryBoundedLatticeHomCarrier` `BoundedOrderHom` `PartOrd.carrier` `BddOrd.toPartOrd` `PartialOrder.toPreorder` `PartOrd.str` `BddOrd.isBoundedOrder` `BoundedOrderHom.instFunLike` `BddOrd.instConcreteCategoryBoundedOrderHomCarrier` `BddLat.hasForgetToBddOrd` `BddOrd.dual`	—	—
`bddLat_dual_comp_forget_to_lat` 📖	mathematical	—	`CategoryTheory.Functor.comp` `BddLat` `BddLat.instLargeCategory` `Lat` `Lat.instCategory` `BddLat.dual` `CategoryTheory.forget₂` `BoundedLatticeHom` `Lat.carrier` `BddLat.toLat` `Lat.str` `BddLat.isBoundedOrder` `BoundedLatticeHom.instFunLike` `BddLat.instConcreteCategoryBoundedLatticeHomCarrier` `LatticeHom` `LatticeHom.instFunLike` `Lat.instConcreteCategoryLatticeHomCarrier` `BddLat.hasForgetToLat` `Lat.dual`	—	—
`bddLat_dual_comp_forget_to_semilatInfCat` 📖	mathematical	—	`CategoryTheory.Functor.comp` `BddLat` `BddLat.instLargeCategory` `SemilatInfCat` `SemilatInfCat.instLargeCategory` `BddLat.dual` `CategoryTheory.forget₂` `BoundedLatticeHom` `Lat.carrier` `BddLat.toLat` `Lat.str` `BddLat.isBoundedOrder` `BoundedLatticeHom.instFunLike` `BddLat.instConcreteCategoryBoundedLatticeHomCarrier` `InfTopHom` `SemilatInfCat.X` `SemilatticeInf.toMin` `SemilatInfCat.isSemilatticeInf` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SemilatInfCat.isOrderTop` `InfTopHom.instFunLike` `SemilatInfCat.instConcreteCategoryInfTopHomX` `BddLat.hasForgetToSemilatInf` `SemilatSupCat` `SemilatSupCat.instLargeCategory` `SupBotHom` `SemilatSupCat.X` `SemilatticeSup.toMax` `SemilatSupCat.isSemilatticeSup` `OrderBot.toBot` `SemilatticeSup.toPartialOrder` `SemilatSupCat.isOrderBot` `SupBotHom.instFunLike` `SemilatSupCat.instConcreteCategorySupBotHomX` `BddLat.hasForgetToSemilatSup` `SemilatSupCat.dual`	—	—
`bddLat_dual_comp_forget_to_semilatSupCat` 📖	mathematical	—	`CategoryTheory.Functor.comp` `BddLat` `BddLat.instLargeCategory` `SemilatSupCat` `SemilatSupCat.instLargeCategory` `BddLat.dual` `CategoryTheory.forget₂` `BoundedLatticeHom` `Lat.carrier` `BddLat.toLat` `Lat.str` `BddLat.isBoundedOrder` `BoundedLatticeHom.instFunLike` `BddLat.instConcreteCategoryBoundedLatticeHomCarrier` `SupBotHom` `SemilatSupCat.X` `SemilatticeSup.toMax` `SemilatSupCat.isSemilatticeSup` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SemilatSupCat.isOrderBot` `SupBotHom.instFunLike` `SemilatSupCat.instConcreteCategorySupBotHomX` `BddLat.hasForgetToSemilatSup` `SemilatInfCat` `SemilatInfCat.instLargeCategory` `InfTopHom` `SemilatInfCat.X` `SemilatticeInf.toMin` `SemilatInfCat.isSemilatticeInf` `OrderTop.toTop` `SemilatticeInf.toPartialOrder` `SemilatInfCat.isOrderTop` `InfTopHom.instFunLike` `SemilatInfCat.instConcreteCategoryInfTopHomX` `BddLat.hasForgetToSemilatInf` `SemilatInfCat.dual`	—	—

---

← Back to Index