Documentation Verification Report

FinPartOrd

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

Statistics

Metric	Count
Definitions `FinPartOrd`, `mk`, `concreteCategory`, `dual`, `dualEquiv`, `hasForgetToFintype`, `hasForgetToPartOrd`, `instCoeSortType`, `instInhabited`, `instPartialOrderCarrier`, `isFintype`, `largeCategory`, `of`, `ofHom`, `toPartOrd`	15
Theorems `mk_hom`, `mk_inv`, `comp_apply`, `dualEquiv_counitIso`, `dualEquiv_functor`, `dualEquiv_inverse`, `dualEquiv_unitIso`, `dual_map`, `hom_comp`, `hom_ext`, `hom_ext_iff`, `hom_hom_comp`, `hom_hom_id`, `hom_hom_ofHom`, `hom_id`, `hom_ofHom`, `id_apply`, `ofHom_hom`, `ofHom_hom_hom`, `FinPartOrd_dual_comp_forget_to_partOrd`	20
Total	35

FinPartOrd

Definitions

Name	Category	Theorems
`concreteCategory` 📖	CompOp	8 math math: `FinBoolAlg.forgetToFinPartOrdFaithful`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_carrier`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_isFintype`, `comp_apply`, `FinPartOrd_dual_comp_forget_to_partOrd`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_map`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_str`, `id_apply`
`dual` 📖	CompOp	6 math math: `dualEquiv_functor`, `dualEquiv_unitIso`, `dualEquiv_counitIso`, `dual_map`, `dualEquiv_inverse`, `FinPartOrd_dual_comp_forget_to_partOrd`
`dualEquiv` 📖	CompOp	4 math math: `dualEquiv_functor`, `dualEquiv_unitIso`, `dualEquiv_counitIso`, `dualEquiv_inverse`
`hasForgetToFintype` 📖	CompOp	—
`hasForgetToPartOrd` 📖	CompOp	1 math math: `FinPartOrd_dual_comp_forget_to_partOrd`
`instCoeSortType` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`instPartialOrderCarrier` 📖	CompOp	15 math math: `dualEquiv_unitIso`, `FinBoolAlg.forgetToFinPartOrdFaithful`, `ofHom_hom_hom`, `dualEquiv_counitIso`, `dual_map`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_carrier`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_isFintype`, `comp_apply`, `Iso.mk_inv`, `FinPartOrd_dual_comp_forget_to_partOrd`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_map`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_str`, `Iso.mk_hom`, `id_apply`, `ofHom_hom`
`isFintype` 📖	CompOp	6 math math: `ofHom_hom_hom`, `dual_map`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_isFintype`, `Iso.mk_inv`, `Iso.mk_hom`, `ofHom_hom`
`largeCategory` 📖	CompOp	19 math math: `dualEquiv_functor`, `dualEquiv_unitIso`, `hom_hom_comp`, `FinBoolAlg.forgetToFinPartOrdFaithful`, `dualEquiv_counitIso`, `dual_map`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_carrier`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_isFintype`, `dualEquiv_inverse`, `comp_apply`, `Iso.mk_inv`, `hom_id`, `FinPartOrd_dual_comp_forget_to_partOrd`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_map`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_str`, `hom_comp`, `Iso.mk_hom`, `id_apply`, `hom_hom_id`
`of` 📖	CompOp	3 math math: `hom_ofHom`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_map`, `hom_hom_ofHom`
`ofHom` 📖	CompOp	7 math math: `hom_ofHom`, `ofHom_hom_hom`, `dual_map`, `Iso.mk_inv`, `Iso.mk_hom`, `ofHom_hom`, `hom_hom_ofHom`
`toPartOrd` 📖	CompOp	22 math math: `dualEquiv_unitIso`, `hom_ofHom`, `hom_hom_comp`, `FinBoolAlg.forgetToFinPartOrdFaithful`, `ofHom_hom_hom`, `dualEquiv_counitIso`, `dual_map`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_carrier`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_isFintype`, `comp_apply`, `Iso.mk_inv`, `hom_id`, `FinPartOrd_dual_comp_forget_to_partOrd`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_map`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_str`, `hom_comp`, `Iso.mk_hom`, `id_apply`, `ofHom_hom`, `hom_hom_id`, `hom_hom_ofHom`, `hom_ext_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `FinPartOrd` `largeCategory` `OrderHom` `PartOrd.carrier` `toPartOrd` `PartialOrder.toPreorder` `instPartialOrderCarrier` `OrderHom.instFunLike` `concreteCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.comp_apply`
`dualEquiv_counitIso` 📖	mathematical	—	`CategoryTheory.Equivalence.counitIso` `FinPartOrd` `largeCategory` `dualEquiv` `CategoryTheory.NatIso.ofComponents` `CategoryTheory.Functor.comp` `dual` `CategoryTheory.Functor.id` `CategoryTheory.Functor.obj` `OrderIso.dualDual` `PartOrd.carrier` `toPartOrd` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderCarrier`	—	—
`dualEquiv_functor` 📖	mathematical	—	`CategoryTheory.Equivalence.functor` `FinPartOrd` `largeCategory` `dualEquiv` `dual`	—	—
`dualEquiv_inverse` 📖	mathematical	—	`CategoryTheory.Equivalence.inverse` `FinPartOrd` `largeCategory` `dualEquiv` `dual`	—	—
`dualEquiv_unitIso` 📖	mathematical	—	`CategoryTheory.Equivalence.unitIso` `FinPartOrd` `largeCategory` `dualEquiv` `CategoryTheory.NatIso.ofComponents` `CategoryTheory.Functor.id` `CategoryTheory.Functor.comp` `dual` `CategoryTheory.Functor.obj` `OrderIso.dualDual` `PartOrd.carrier` `toPartOrd` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderCarrier`	—	—
`dual_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `FinPartOrd` `largeCategory` `dual` `ofHom` `OrderDual` `PartOrd.carrier` `toPartOrd` `OrderDual.instPartialOrder` `instPartialOrderCarrier` `OrderDual.fintype` `isFintype` `DFunLike.coe` `Equiv` `OrderHom` `PartialOrder.toPreorder` `PartOrd.str` `OrderDual.instPreorder` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderHom.dual` `PartOrd.Hom.hom` `CategoryTheory.InducedCategory.Hom.hom` `PartOrd` `PartOrd.instCategory`	—	—
`hom_comp` 📖	mathematical	—	`PartOrd.Hom.hom` `toPartOrd` `CategoryTheory.InducedCategory.Hom.hom` `FinPartOrd` `PartOrd` `PartOrd.instCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `largeCategory` `OrderHom.comp` `PartOrd.carrier` `PartialOrder.toPreorder` `PartOrd.str`	—	`hom_hom_comp`
`hom_ext` 📖	—	`PartOrd.Hom.hom` `toPartOrd` `CategoryTheory.InducedCategory.Hom.hom` `FinPartOrd` `PartOrd` `PartOrd.instCategory`	—	—	`CategoryTheory.InducedCategory.hom_ext` `CategoryTheory.ConcreteCategory.ext`
`hom_ext_iff` 📖	mathematical	—	`PartOrd.Hom.hom` `toPartOrd` `CategoryTheory.InducedCategory.Hom.hom` `FinPartOrd` `PartOrd` `PartOrd.instCategory`	—	`hom_ext`
`hom_hom_comp` 📖	mathematical	—	`PartOrd.Hom.hom` `toPartOrd` `CategoryTheory.InducedCategory.Hom.hom` `FinPartOrd` `PartOrd` `PartOrd.instCategory` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `largeCategory` `OrderHom.comp` `PartOrd.carrier` `PartialOrder.toPreorder` `PartOrd.str`	—	—
`hom_hom_id` 📖	mathematical	—	`PartOrd.Hom.hom` `toPartOrd` `CategoryTheory.InducedCategory.Hom.hom` `FinPartOrd` `PartOrd` `PartOrd.instCategory` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `largeCategory` `OrderHom.id` `PartOrd.carrier` `PartialOrder.toPreorder` `PartOrd.str`	—	—
`hom_hom_ofHom` 📖	mathematical	—	`PartOrd.Hom.hom` `toPartOrd` `of` `CategoryTheory.InducedCategory.Hom.hom` `FinPartOrd` `PartOrd` `PartOrd.instCategory` `ofHom`	—	—
`hom_id` 📖	mathematical	—	`PartOrd.Hom.hom` `toPartOrd` `CategoryTheory.InducedCategory.Hom.hom` `FinPartOrd` `PartOrd` `PartOrd.instCategory` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct` `largeCategory` `OrderHom.id` `PartOrd.carrier` `PartialOrder.toPreorder` `PartOrd.str`	—	`hom_hom_id`
`hom_ofHom` 📖	mathematical	—	`PartOrd.Hom.hom` `toPartOrd` `of` `CategoryTheory.InducedCategory.Hom.hom` `FinPartOrd` `PartOrd` `PartOrd.instCategory` `ofHom`	—	`hom_hom_ofHom`
`id_apply` 📖	mathematical	—	`DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `FinPartOrd` `largeCategory` `OrderHom` `PartOrd.carrier` `toPartOrd` `PartialOrder.toPreorder` `instPartialOrderCarrier` `OrderHom.instFunLike` `concreteCategory` `CategoryTheory.CategoryStruct.id` `CategoryTheory.Category.toCategoryStruct`	—	`CategoryTheory.id_apply`
`ofHom_hom` 📖	mathematical	—	`ofHom` `PartOrd.carrier` `toPartOrd` `instPartialOrderCarrier` `isFintype` `PartOrd.Hom.hom` `CategoryTheory.InducedCategory.Hom.hom` `FinPartOrd` `PartOrd` `PartOrd.instCategory`	—	`ofHom_hom_hom`
`ofHom_hom_hom` 📖	mathematical	—	`ofHom` `PartOrd.carrier` `toPartOrd` `instPartialOrderCarrier` `isFintype` `PartOrd.Hom.hom` `CategoryTheory.InducedCategory.Hom.hom` `FinPartOrd` `PartOrd` `PartOrd.instCategory`	—	—

FinPartOrd.Iso

Definitions

Name	Category	Theorems
`mk` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `FinPartOrd` `FinPartOrd.largeCategory` `FinPartOrd.ofHom` `PartOrd.carrier` `PartOrd.str` `FinPartOrd.isFintype` `OrderHomClass.toOrderHom` `OrderIso` `FinPartOrd.toPartOrd` `Preorder.toLE` `PartialOrder.toPreorder` `FinPartOrd.instPartialOrderCarrier` `instFunLikeOrderIso`	—	—
`mk_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `FinPartOrd` `FinPartOrd.largeCategory` `FinPartOrd.ofHom` `PartOrd.carrier` `PartOrd.str` `FinPartOrd.isFintype` `OrderHomClass.toOrderHom` `OrderIso` `FinPartOrd.toPartOrd` `Preorder.toLE` `PartialOrder.toPreorder` `FinPartOrd.instPartialOrderCarrier` `instFunLikeOrderIso` `OrderIso.symm`	—	—

(root)

Definitions

Name	Category	Theorems
`FinPartOrd` 📖	CompData	24 math math: `FinPartOrd.dualEquiv_functor`, `FinPartOrd.dualEquiv_unitIso`, `FinPartOrd.hom_ofHom`, `FinPartOrd.hom_hom_comp`, `FinBoolAlg.forgetToFinPartOrdFaithful`, `FinPartOrd.ofHom_hom_hom`, `FinPartOrd.dualEquiv_counitIso`, `FinPartOrd.dual_map`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_carrier`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_isFintype`, `FinPartOrd.dualEquiv_inverse`, `FinPartOrd.comp_apply`, `FinPartOrd.Iso.mk_inv`, `FinPartOrd.hom_id`, `FinPartOrd_dual_comp_forget_to_partOrd`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_map`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_str`, `FinPartOrd.hom_comp`, `FinPartOrd.Iso.mk_hom`, `FinPartOrd.id_apply`, `FinPartOrd.ofHom_hom`, `FinPartOrd.hom_hom_id`, `FinPartOrd.hom_hom_ofHom`, `FinPartOrd.hom_ext_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`FinPartOrd_dual_comp_forget_to_partOrd` 📖	mathematical	—	`CategoryTheory.Functor.comp` `FinPartOrd` `FinPartOrd.largeCategory` `PartOrd` `PartOrd.instCategory` `FinPartOrd.dual` `CategoryTheory.forget₂` `OrderHom` `PartOrd.carrier` `FinPartOrd.toPartOrd` `PartialOrder.toPreorder` `FinPartOrd.instPartialOrderCarrier` `OrderHom.instFunLike` `FinPartOrd.concreteCategory` `PartOrd.str` `PartOrd.instConcreteCategoryOrderHomCarrier` `FinPartOrd.hasForgetToPartOrd` `PartOrd.dual`	—	—

---

← Back to Index