Documentation Verification Report

CompleteLat

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

Statistics

Metric	Count
Definitions `CompleteLat`, `mk`, `carrier`, `dual`, `dualEquiv`, `hasForgetToBddLat`, `instCoeSortType`, `instConcreteCategoryCompleteLatticeHomCarrier`, `instInhabited`, `instLargeCategory`, `str`	11
Theorems `mk_hom`, `mk_inv`, `coe_of`, `dualEquiv_functor`, `dualEquiv_inverse`, `dual_map`, `completeLat_dual_comp_forget_to_bddLat`	7
Total	18

CompleteLat

Definitions

Name	Category	Theorems
`carrier` 📖	CompOp	5 math math: `coe_of`, `dual_map`, `Iso.mk_hom`, `completeLat_dual_comp_forget_to_bddLat`, `Iso.mk_inv`
`dual` 📖	CompOp	4 math math: `dualEquiv_functor`, `dual_map`, `dualEquiv_inverse`, `completeLat_dual_comp_forget_to_bddLat`
`dualEquiv` 📖	CompOp	2 math math: `dualEquiv_functor`, `dualEquiv_inverse`
`hasForgetToBddLat` 📖	CompOp	1 math math: `completeLat_dual_comp_forget_to_bddLat`
`instCoeSortType` 📖	CompOp	—
`instConcreteCategoryCompleteLatticeHomCarrier` 📖	CompOp	3 math math: `Iso.mk_hom`, `completeLat_dual_comp_forget_to_bddLat`, `Iso.mk_inv`
`instInhabited` 📖	CompOp	—
`instLargeCategory` 📖	CompOp	6 math math: `dualEquiv_functor`, `dual_map`, `dualEquiv_inverse`, `Iso.mk_hom`, `completeLat_dual_comp_forget_to_bddLat`, `Iso.mk_inv`
`str` 📖	CompOp	4 math math: `dual_map`, `Iso.mk_hom`, `completeLat_dual_comp_forget_to_bddLat`, `Iso.mk_inv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_of` 📖	mathematical	—	`carrier` `of`	—	—
`dualEquiv_functor` 📖	mathematical	—	`CategoryTheory.Equivalence.functor` `CompleteLat` `instLargeCategory` `dualEquiv` `dual`	—	—
`dualEquiv_inverse` 📖	mathematical	—	`CategoryTheory.Equivalence.inverse` `CompleteLat` `instLargeCategory` `dualEquiv` `dual`	—	—
`dual_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CompleteLat` `instLargeCategory` `dual` `DFunLike.coe` `Equiv` `CompleteLatticeHom` `carrier` `str` `OrderDual` `OrderDual.instCompleteLattice` `EquivLike.toFunLike` `Equiv.instEquivLike` `CompleteLatticeHom.dual`	—	—

CompleteLat.Iso

Definitions

Name	Category	Theorems
`mk` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `CompleteLat` `CompleteLat.instLargeCategory` `CategoryTheory.ConcreteCategory.ofHom` `CompleteLatticeHom` `CompleteLat.carrier` `CompleteLat.str` `CompleteLatticeHom.instFunLike` `CompleteLat.instConcreteCategoryCompleteLatticeHomCarrier` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf` `DFunLike.coe` `OrderIso` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `instFunLikeOrderIso`	—	—
`mk_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `CompleteLat` `CompleteLat.instLargeCategory` `CategoryTheory.ConcreteCategory.ofHom` `CompleteLatticeHom` `CompleteLat.carrier` `CompleteLat.str` `CompleteLatticeHom.instFunLike` `CompleteLat.instConcreteCategoryCompleteLatticeHomCarrier` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf` `DFunLike.coe` `OrderIso` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteSemilatticeInf.toPartialOrder` `instFunLikeOrderIso` `OrderIso.symm`	—	—

(root)

Definitions

Name	Category	Theorems
`CompleteLat` 📖	CompData	6 math math: `CompleteLat.dualEquiv_functor`, `CompleteLat.dual_map`, `CompleteLat.dualEquiv_inverse`, `CompleteLat.Iso.mk_hom`, `completeLat_dual_comp_forget_to_bddLat`, `CompleteLat.Iso.mk_inv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`completeLat_dual_comp_forget_to_bddLat` 📖	mathematical	—	`CategoryTheory.Functor.comp` `CompleteLat` `CompleteLat.instLargeCategory` `BddLat` `BddLat.instLargeCategory` `CompleteLat.dual` `CategoryTheory.forget₂` `CompleteLatticeHom` `CompleteLat.carrier` `CompleteLat.str` `CompleteLatticeHom.instFunLike` `CompleteLat.instConcreteCategoryCompleteLatticeHomCarrier` `BoundedLatticeHom` `Lat.carrier` `BddLat.toLat` `Lat.str` `BddLat.isBoundedOrder` `BoundedLatticeHom.instFunLike` `BddLat.instConcreteCategoryBoundedLatticeHomCarrier` `CompleteLat.hasForgetToBddLat` `BddLat.dual`	—	—

---

← Back to Index