Documentation Verification Report

Semilat

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

Statistics

Metric	Count
Definitions `SemilatInfCat`, `mk`, `X`, `dual`, `hasForgetToPartOrd`, `instCoeSortType`, `instConcreteCategoryInfTopHomX`, `instInhabited`, `instLargeCategory`, `isOrderTop`, `isSemilatticeInf`, `SemilatSupCat`, `mk`, `X`, `dual`, `hasForgetToPartOrd`, `instCoeSortType`, `instConcreteCategorySupBotHomX`, `instInhabited`, `instLargeCategory`, `isOrderBot`, `isSemilatticeSup`, `SemilatSupCatEquivSemilatInfCat`	23
Theorems `mk_hom_toFun`, `mk_inv_toFun`, `coe_forget_to_partOrd`, `coe_of`, `dual_map`, `dual_obj_X`, `dual_obj_isOrderBot`, `dual_obj_isSemilatticeSup`, `SemilatInfCat_dual_comp_forget_to_partOrd`, `mk_hom_toFun`, `mk_inv_toFun`, `coe_forget_to_partOrd`, `coe_of`, `dual_map`, `SemilatSupCatEquivSemilatInfCat_functor`, `SemilatSupCatEquivSemilatInfCat_inverse`, `SemilatSupCat_dual_comp_forget_to_partOrd`	17
Total	40

SemilatInfCat

Definitions

Name	Category	Theorems
`X` 📖	CompOp	14 math math: `SemilatInfCat_dual_comp_forget_to_partOrd`, `dual_obj_isOrderBot`, `dual_obj_X`, `BddLat.forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd`, `coe_forget_to_partOrd`, `bddLat_dual_comp_forget_to_semilatSupCat`, `bddLat_dual_comp_forget_to_semilatInfCat`, `coe_of`, `Iso.mk_inv_toFun`, `dual_map`, `Iso.mk_hom_toFun`, `BddLat.coe_forget_to_semilatInf`, `SemilatSupCat_dual_comp_forget_to_partOrd`, `dual_obj_isSemilatticeSup`
`dual` 📖	CompOp	7 math math: `SemilatInfCat_dual_comp_forget_to_partOrd`, `dual_obj_isOrderBot`, `dual_obj_X`, `bddLat_dual_comp_forget_to_semilatSupCat`, `SemilatSupCatEquivSemilatInfCat_inverse`, `dual_map`, `dual_obj_isSemilatticeSup`
`hasForgetToPartOrd` 📖	CompOp	4 math math: `SemilatInfCat_dual_comp_forget_to_partOrd`, `BddLat.forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd`, `coe_forget_to_partOrd`, `SemilatSupCat_dual_comp_forget_to_partOrd`
`instCoeSortType` 📖	CompOp	—
`instConcreteCategoryInfTopHomX` 📖	CompOp	7 math math: `SemilatInfCat_dual_comp_forget_to_partOrd`, `BddLat.forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd`, `coe_forget_to_partOrd`, `bddLat_dual_comp_forget_to_semilatSupCat`, `bddLat_dual_comp_forget_to_semilatInfCat`, `BddLat.coe_forget_to_semilatInf`, `SemilatSupCat_dual_comp_forget_to_partOrd`
`instInhabited` 📖	CompOp	—
`instLargeCategory` 📖	CompOp	16 math math: `SemilatInfCat_dual_comp_forget_to_partOrd`, `dual_obj_isOrderBot`, `dual_obj_X`, `SemilatSupCatEquivSemilatInfCat_functor`, `BddLat.forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd`, `SemilatSupCat.dual_map`, `coe_forget_to_partOrd`, `bddLat_dual_comp_forget_to_semilatSupCat`, `bddLat_dual_comp_forget_to_semilatInfCat`, `SemilatSupCatEquivSemilatInfCat_inverse`, `Iso.mk_inv_toFun`, `dual_map`, `Iso.mk_hom_toFun`, `BddLat.coe_forget_to_semilatInf`, `SemilatSupCat_dual_comp_forget_to_partOrd`, `dual_obj_isSemilatticeSup`
`isOrderTop` 📖	CompOp	11 math math: `SemilatInfCat_dual_comp_forget_to_partOrd`, `dual_obj_isOrderBot`, `BddLat.forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd`, `coe_forget_to_partOrd`, `bddLat_dual_comp_forget_to_semilatSupCat`, `bddLat_dual_comp_forget_to_semilatInfCat`, `Iso.mk_inv_toFun`, `dual_map`, `Iso.mk_hom_toFun`, `BddLat.coe_forget_to_semilatInf`, `SemilatSupCat_dual_comp_forget_to_partOrd`
`isSemilatticeInf` 📖	CompOp	12 math math: `SemilatInfCat_dual_comp_forget_to_partOrd`, `dual_obj_isOrderBot`, `BddLat.forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd`, `coe_forget_to_partOrd`, `bddLat_dual_comp_forget_to_semilatSupCat`, `bddLat_dual_comp_forget_to_semilatInfCat`, `Iso.mk_inv_toFun`, `dual_map`, `Iso.mk_hom_toFun`, `BddLat.coe_forget_to_semilatInf`, `SemilatSupCat_dual_comp_forget_to_partOrd`, `dual_obj_isSemilatticeSup`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_forget_to_partOrd` 📖	mathematical	—	`PartOrd.carrier` `CategoryTheory.Functor.obj` `SemilatInfCat` `instLargeCategory` `PartOrd` `PartOrd.instCategory` `CategoryTheory.forget₂` `InfTopHom` `X` `SemilatticeInf.toMin` `isSemilatticeInf` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `isOrderTop` `InfTopHom.instFunLike` `instConcreteCategoryInfTopHomX` `OrderHom` `PartOrd.str` `OrderHom.instFunLike` `PartOrd.instConcreteCategoryOrderHomCarrier` `hasForgetToPartOrd`	—	—
`coe_of` 📖	mathematical	—	`X` `of`	—	—
`dual_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `SemilatInfCat` `instLargeCategory` `SemilatSupCat` `SemilatSupCat.instLargeCategory` `dual` `DFunLike.coe` `Equiv` `InfTopHom` `X` `SemilatticeInf.toMin` `isSemilatticeInf` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `isOrderTop` `SupBotHom` `OrderDual` `OrderDual.instSup` `OrderDual.instBot` `EquivLike.toFunLike` `Equiv.instEquivLike` `InfTopHom.dual`	—	—
`dual_obj_X` 📖	mathematical	—	`SemilatSupCat.X` `CategoryTheory.Functor.obj` `SemilatInfCat` `instLargeCategory` `SemilatSupCat` `SemilatSupCat.instLargeCategory` `dual` `OrderDual` `X`	—	—
`dual_obj_isOrderBot` 📖	mathematical	—	`SemilatSupCat.isOrderBot` `CategoryTheory.Functor.obj` `SemilatInfCat` `instLargeCategory` `SemilatSupCat` `SemilatSupCat.instLargeCategory` `dual` `OrderDual.instOrderBot` `X` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `isSemilatticeInf` `isOrderTop`	—	—
`dual_obj_isSemilatticeSup` 📖	mathematical	—	`SemilatSupCat.isSemilatticeSup` `CategoryTheory.Functor.obj` `SemilatInfCat` `instLargeCategory` `SemilatSupCat` `SemilatSupCat.instLargeCategory` `dual` `OrderDual.instSemilatticeSup` `X` `isSemilatticeInf`	—	—

SemilatInfCat.Iso

Definitions

Name	Category	Theorems
`mk` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk_hom_toFun` 📖	mathematical	—	`DFunLike.coe` `InfTopHom` `SemilatInfCat.X` `SemilatticeInf.toMin` `SemilatInfCat.isSemilatticeInf` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SemilatInfCat.isOrderTop` `InfTopHom.instFunLike` `CategoryTheory.Iso.hom` `SemilatInfCat` `SemilatInfCat.instLargeCategory` `OrderIso` `instFunLikeOrderIso`	—	—
`mk_inv_toFun` 📖	mathematical	—	`DFunLike.coe` `InfTopHom` `SemilatInfCat.X` `SemilatticeInf.toMin` `SemilatInfCat.isSemilatticeInf` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SemilatInfCat.isOrderTop` `InfTopHom.instFunLike` `CategoryTheory.Iso.inv` `SemilatInfCat` `SemilatInfCat.instLargeCategory` `OrderIso` `instFunLikeOrderIso` `OrderIso.symm`	—	—

SemilatSupCat

Definitions

Name	Category	Theorems
`X` 📖	CompOp	12 math math: `SemilatInfCat_dual_comp_forget_to_partOrd`, `Iso.mk_inv_toFun`, `BddLat.forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd`, `SemilatInfCat.dual_obj_X`, `dual_map`, `bddLat_dual_comp_forget_to_semilatSupCat`, `bddLat_dual_comp_forget_to_semilatInfCat`, `Iso.mk_hom_toFun`, `BddLat.coe_forget_to_semilatSup`, `coe_of`, `SemilatSupCat_dual_comp_forget_to_partOrd`, `coe_forget_to_partOrd`
`dual` 📖	CompOp	4 math math: `SemilatSupCatEquivSemilatInfCat_functor`, `dual_map`, `bddLat_dual_comp_forget_to_semilatInfCat`, `SemilatSupCat_dual_comp_forget_to_partOrd`
`hasForgetToPartOrd` 📖	CompOp	4 math math: `SemilatInfCat_dual_comp_forget_to_partOrd`, `BddLat.forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd`, `SemilatSupCat_dual_comp_forget_to_partOrd`, `coe_forget_to_partOrd`
`instCoeSortType` 📖	CompOp	—
`instConcreteCategorySupBotHomX` 📖	CompOp	7 math math: `SemilatInfCat_dual_comp_forget_to_partOrd`, `BddLat.forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd`, `bddLat_dual_comp_forget_to_semilatSupCat`, `bddLat_dual_comp_forget_to_semilatInfCat`, `BddLat.coe_forget_to_semilatSup`, `SemilatSupCat_dual_comp_forget_to_partOrd`, `coe_forget_to_partOrd`
`instInhabited` 📖	CompOp	—
`instLargeCategory` 📖	CompOp	16 math math: `SemilatInfCat_dual_comp_forget_to_partOrd`, `Iso.mk_inv_toFun`, `SemilatInfCat.dual_obj_isOrderBot`, `BddLat.forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd`, `SemilatInfCat.dual_obj_X`, `SemilatSupCatEquivSemilatInfCat_functor`, `dual_map`, `bddLat_dual_comp_forget_to_semilatSupCat`, `bddLat_dual_comp_forget_to_semilatInfCat`, `SemilatSupCatEquivSemilatInfCat_inverse`, `Iso.mk_hom_toFun`, `SemilatInfCat.dual_map`, `BddLat.coe_forget_to_semilatSup`, `SemilatSupCat_dual_comp_forget_to_partOrd`, `SemilatInfCat.dual_obj_isSemilatticeSup`, `coe_forget_to_partOrd`
`isOrderBot` 📖	CompOp	11 math math: `SemilatInfCat_dual_comp_forget_to_partOrd`, `Iso.mk_inv_toFun`, `SemilatInfCat.dual_obj_isOrderBot`, `BddLat.forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd`, `dual_map`, `bddLat_dual_comp_forget_to_semilatSupCat`, `bddLat_dual_comp_forget_to_semilatInfCat`, `Iso.mk_hom_toFun`, `BddLat.coe_forget_to_semilatSup`, `SemilatSupCat_dual_comp_forget_to_partOrd`, `coe_forget_to_partOrd`
`isSemilatticeSup` 📖	CompOp	11 math math: `SemilatInfCat_dual_comp_forget_to_partOrd`, `Iso.mk_inv_toFun`, `BddLat.forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd`, `dual_map`, `bddLat_dual_comp_forget_to_semilatSupCat`, `bddLat_dual_comp_forget_to_semilatInfCat`, `Iso.mk_hom_toFun`, `BddLat.coe_forget_to_semilatSup`, `SemilatSupCat_dual_comp_forget_to_partOrd`, `SemilatInfCat.dual_obj_isSemilatticeSup`, `coe_forget_to_partOrd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_forget_to_partOrd` 📖	mathematical	—	`PartOrd.carrier` `CategoryTheory.Functor.obj` `SemilatSupCat` `instLargeCategory` `PartOrd` `PartOrd.instCategory` `CategoryTheory.forget₂` `SupBotHom` `X` `SemilatticeSup.toMax` `isSemilatticeSup` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `isOrderBot` `SupBotHom.instFunLike` `instConcreteCategorySupBotHomX` `OrderHom` `PartOrd.str` `OrderHom.instFunLike` `PartOrd.instConcreteCategoryOrderHomCarrier` `hasForgetToPartOrd`	—	—
`coe_of` 📖	mathematical	—	`X` `of`	—	—
`dual_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `SemilatSupCat` `instLargeCategory` `SemilatInfCat` `SemilatInfCat.instLargeCategory` `dual` `DFunLike.coe` `Equiv` `SupBotHom` `X` `SemilatticeSup.toMax` `isSemilatticeSup` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `isOrderBot` `InfTopHom` `OrderDual` `OrderDual.instInf` `OrderDual.instTop` `EquivLike.toFunLike` `Equiv.instEquivLike` `SupBotHom.dual`	—	—

SemilatSupCat.Iso

Definitions

Name	Category	Theorems
`mk` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk_hom_toFun` 📖	mathematical	—	`DFunLike.coe` `SupBotHom` `SemilatSupCat.X` `SemilatticeSup.toMax` `SemilatSupCat.isSemilatticeSup` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SemilatSupCat.isOrderBot` `SupBotHom.instFunLike` `CategoryTheory.Iso.hom` `SemilatSupCat` `SemilatSupCat.instLargeCategory` `OrderIso` `instFunLikeOrderIso`	—	—
`mk_inv_toFun` 📖	mathematical	—	`DFunLike.coe` `SupBotHom` `SemilatSupCat.X` `SemilatticeSup.toMax` `SemilatSupCat.isSemilatticeSup` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SemilatSupCat.isOrderBot` `SupBotHom.instFunLike` `CategoryTheory.Iso.inv` `SemilatSupCat` `SemilatSupCat.instLargeCategory` `OrderIso` `instFunLikeOrderIso` `OrderIso.symm`	—	—

(root)

Definitions

Name	Category	Theorems
`SemilatInfCat` 📖	CompData	16 math math: `SemilatInfCat_dual_comp_forget_to_partOrd`, `SemilatInfCat.dual_obj_isOrderBot`, `SemilatInfCat.dual_obj_X`, `SemilatSupCatEquivSemilatInfCat_functor`, `BddLat.forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd`, `SemilatSupCat.dual_map`, `SemilatInfCat.coe_forget_to_partOrd`, `bddLat_dual_comp_forget_to_semilatSupCat`, `bddLat_dual_comp_forget_to_semilatInfCat`, `SemilatSupCatEquivSemilatInfCat_inverse`, `SemilatInfCat.Iso.mk_inv_toFun`, `SemilatInfCat.dual_map`, `SemilatInfCat.Iso.mk_hom_toFun`, `BddLat.coe_forget_to_semilatInf`, `SemilatSupCat_dual_comp_forget_to_partOrd`, `SemilatInfCat.dual_obj_isSemilatticeSup`
`SemilatSupCat` 📖	CompData	16 math math: `SemilatInfCat_dual_comp_forget_to_partOrd`, `SemilatSupCat.Iso.mk_inv_toFun`, `SemilatInfCat.dual_obj_isOrderBot`, `BddLat.forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd`, `SemilatInfCat.dual_obj_X`, `SemilatSupCatEquivSemilatInfCat_functor`, `SemilatSupCat.dual_map`, `bddLat_dual_comp_forget_to_semilatSupCat`, `bddLat_dual_comp_forget_to_semilatInfCat`, `SemilatSupCatEquivSemilatInfCat_inverse`, `SemilatSupCat.Iso.mk_hom_toFun`, `SemilatInfCat.dual_map`, `BddLat.coe_forget_to_semilatSup`, `SemilatSupCat_dual_comp_forget_to_partOrd`, `SemilatInfCat.dual_obj_isSemilatticeSup`, `SemilatSupCat.coe_forget_to_partOrd`
`SemilatSupCatEquivSemilatInfCat` 📖	CompOp	2 math math: `SemilatSupCatEquivSemilatInfCat_functor`, `SemilatSupCatEquivSemilatInfCat_inverse`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`SemilatInfCat_dual_comp_forget_to_partOrd` 📖	mathematical	—	`CategoryTheory.Functor.comp` `SemilatInfCat` `SemilatInfCat.instLargeCategory` `SemilatSupCat` `SemilatSupCat.instLargeCategory` `PartOrd` `PartOrd.instCategory` `SemilatInfCat.dual` `CategoryTheory.forget₂` `SupBotHom` `SemilatSupCat.X` `SemilatticeSup.toMax` `SemilatSupCat.isSemilatticeSup` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `SemilatSupCat.isOrderBot` `SupBotHom.instFunLike` `SemilatSupCat.instConcreteCategorySupBotHomX` `OrderHom` `PartOrd.carrier` `PartOrd.str` `OrderHom.instFunLike` `PartOrd.instConcreteCategoryOrderHomCarrier` `SemilatSupCat.hasForgetToPartOrd` `InfTopHom` `SemilatInfCat.X` `SemilatticeInf.toMin` `SemilatInfCat.isSemilatticeInf` `OrderTop.toTop` `SemilatticeInf.toPartialOrder` `SemilatInfCat.isOrderTop` `InfTopHom.instFunLike` `SemilatInfCat.instConcreteCategoryInfTopHomX` `SemilatInfCat.hasForgetToPartOrd` `PartOrd.dual`	—	—
`SemilatSupCatEquivSemilatInfCat_functor` 📖	mathematical	—	`CategoryTheory.Equivalence.functor` `SemilatSupCat` `SemilatInfCat` `SemilatSupCat.instLargeCategory` `SemilatInfCat.instLargeCategory` `SemilatSupCatEquivSemilatInfCat` `SemilatSupCat.dual`	—	—
`SemilatSupCatEquivSemilatInfCat_inverse` 📖	mathematical	—	`CategoryTheory.Equivalence.inverse` `SemilatSupCat` `SemilatInfCat` `SemilatSupCat.instLargeCategory` `SemilatInfCat.instLargeCategory` `SemilatSupCatEquivSemilatInfCat` `SemilatInfCat.dual`	—	—
`SemilatSupCat_dual_comp_forget_to_partOrd` 📖	mathematical	—	`CategoryTheory.Functor.comp` `SemilatSupCat` `SemilatSupCat.instLargeCategory` `SemilatInfCat` `SemilatInfCat.instLargeCategory` `PartOrd` `PartOrd.instCategory` `SemilatSupCat.dual` `CategoryTheory.forget₂` `InfTopHom` `SemilatInfCat.X` `SemilatticeInf.toMin` `SemilatInfCat.isSemilatticeInf` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `SemilatInfCat.isOrderTop` `InfTopHom.instFunLike` `SemilatInfCat.instConcreteCategoryInfTopHomX` `OrderHom` `PartOrd.carrier` `PartOrd.str` `OrderHom.instFunLike` `PartOrd.instConcreteCategoryOrderHomCarrier` `SemilatInfCat.hasForgetToPartOrd` `SupBotHom` `SemilatSupCat.X` `SemilatticeSup.toMax` `SemilatSupCat.isSemilatticeSup` `OrderBot.toBot` `SemilatticeSup.toPartialOrder` `SemilatSupCat.isOrderBot` `SupBotHom.instFunLike` `SemilatSupCat.instConcreteCategorySupBotHomX` `SemilatSupCat.hasForgetToPartOrd` `PartOrd.dual`	—	—

---

← Back to Index