Documentation Verification Report

FinBoolAlg

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

Statistics

Metric	Count
Definitions `FinBoolAlg`, `mk`, `concreteCategory`, `dual`, `dualEquiv`, `hasForgetToBoolAlg`, `hasForgetToFinBddDistLat`, `hasForgetToFinPartOrd`, `instCoeSortType`, `instInhabited`, `isFintype`, `largeCategory`, `of`, `toBoolAlg`, `fintypeToFinBoolAlgOp`	15
Theorems `mk_hom`, `mk_inv`, `coe_of`, `dualEquiv_functor`, `dualEquiv_inverse`, `dual_map`, `forgetToBoolAlgFaithful`, `forgetToBoolAlg_full`, `forgetToFinPartOrdFaithful`, `hasForgetToFinPartOrd_forget₂_map`, `hasForgetToFinPartOrd_forget₂_obj_carrier`, `hasForgetToFinPartOrd_forget₂_obj_isFintype`, `hasForgetToFinPartOrd_forget₂_obj_str`, `finBoolAlg_dual_comp_forget_to_finBddDistLat`, `fintypeToFinBoolAlgOp_map`, `fintypeToFinBoolAlgOp_obj`	16
Total	31

FinBoolAlg

Definitions

Name	Category	Theorems
`concreteCategory` 📖	CompOp	8 math math: `forgetToFinPartOrdFaithful`, `hasForgetToFinPartOrd_forget₂_obj_carrier`, `hasForgetToFinPartOrd_forget₂_obj_isFintype`, `finBoolAlg_dual_comp_forget_to_finBddDistLat`, `hasForgetToFinPartOrd_forget₂_map`, `forgetToBoolAlg_full`, `hasForgetToFinPartOrd_forget₂_obj_str`, `forgetToBoolAlgFaithful`
`dual` 📖	CompOp	4 math math: `dualEquiv_inverse`, `dualEquiv_functor`, `finBoolAlg_dual_comp_forget_to_finBddDistLat`, `dual_map`
`dualEquiv` 📖	CompOp	2 math math: `dualEquiv_inverse`, `dualEquiv_functor`
`hasForgetToBoolAlg` 📖	CompOp	2 math math: `forgetToBoolAlg_full`, `forgetToBoolAlgFaithful`
`hasForgetToFinBddDistLat` 📖	CompOp	1 math math: `finBoolAlg_dual_comp_forget_to_finBddDistLat`
`hasForgetToFinPartOrd` 📖	CompOp	5 math math: `forgetToFinPartOrdFaithful`, `hasForgetToFinPartOrd_forget₂_obj_carrier`, `hasForgetToFinPartOrd_forget₂_obj_isFintype`, `hasForgetToFinPartOrd_forget₂_map`, `hasForgetToFinPartOrd_forget₂_obj_str`
`instCoeSortType` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`isFintype` 📖	CompOp	3 math math: `hasForgetToFinPartOrd_forget₂_obj_isFintype`, `hasForgetToFinPartOrd_forget₂_map`, `dual_map`
`largeCategory` 📖	CompOp	15 math math: `dualEquiv_inverse`, `forgetToFinPartOrdFaithful`, `dualEquiv_functor`, `fintypeToFinBoolAlgOp_map`, `hasForgetToFinPartOrd_forget₂_obj_carrier`, `hasForgetToFinPartOrd_forget₂_obj_isFintype`, `Iso.mk_inv`, `finBoolAlg_dual_comp_forget_to_finBddDistLat`, `hasForgetToFinPartOrd_forget₂_map`, `forgetToBoolAlg_full`, `Iso.mk_hom`, `hasForgetToFinPartOrd_forget₂_obj_str`, `dual_map`, `fintypeToFinBoolAlgOp_obj`, `forgetToBoolAlgFaithful`
`of` 📖	CompOp	4 math math: `coe_of`, `fintypeToFinBoolAlgOp_map`, `dual_map`, `fintypeToFinBoolAlgOp_obj`
`toBoolAlg` 📖	CompOp	13 math math: `coe_of`, `forgetToFinPartOrdFaithful`, `fintypeToFinBoolAlgOp_map`, `hasForgetToFinPartOrd_forget₂_obj_carrier`, `hasForgetToFinPartOrd_forget₂_obj_isFintype`, `Iso.mk_inv`, `finBoolAlg_dual_comp_forget_to_finBddDistLat`, `hasForgetToFinPartOrd_forget₂_map`, `forgetToBoolAlg_full`, `Iso.mk_hom`, `hasForgetToFinPartOrd_forget₂_obj_str`, `dual_map`, `forgetToBoolAlgFaithful`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_of` 📖	mathematical	—	`BoolAlg.carrier` `toBoolAlg` `of`	—	—
`dualEquiv_functor` 📖	mathematical	—	`CategoryTheory.Equivalence.functor` `FinBoolAlg` `largeCategory` `dualEquiv` `dual`	—	—
`dualEquiv_inverse` 📖	mathematical	—	`CategoryTheory.Equivalence.inverse` `FinBoolAlg` `largeCategory` `dualEquiv` `dual`	—	—
`dual_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `FinBoolAlg` `largeCategory` `dual` `CategoryTheory.InducedCategory.homMk` `BoolAlg` `BoolAlg.instCategory` `toBoolAlg` `of` `OrderDual` `BoolAlg.carrier` `OrderDual.instBooleanAlgebra` `BoolAlg.str` `OrderDual.fintype` `isFintype` `BoolAlg.ofHom` `DFunLike.coe` `Equiv` `BoundedLatticeHom` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `BooleanAlgebra.toBoundedOrder` `OrderDual.instLattice` `OrderDual.instBoundedOrder` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `EquivLike.toFunLike` `Equiv.instEquivLike` `BoundedLatticeHom.dual` `BoolAlg.Hom.hom` `CategoryTheory.InducedCategory.Hom.hom`	—	—
`forgetToBoolAlgFaithful` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `FinBoolAlg` `largeCategory` `BoolAlg` `BoolAlg.instCategory` `CategoryTheory.forget₂` `BoundedLatticeHom` `BoolAlg.carrier` `toBoolAlg` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `BoolAlg.str` `BooleanAlgebra.toBoundedOrder` `BoundedLatticeHom.instFunLike` `concreteCategory` `BoolAlg.instConcreteCategoryBoundedLatticeHomCarrier` `hasForgetToBoolAlg`	—	`CategoryTheory.InducedCategory.faithful`
`forgetToBoolAlg_full` 📖	mathematical	—	`CategoryTheory.Functor.Full` `FinBoolAlg` `largeCategory` `BoolAlg` `BoolAlg.instCategory` `CategoryTheory.forget₂` `BoundedLatticeHom` `BoolAlg.carrier` `toBoolAlg` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `BoolAlg.str` `BooleanAlgebra.toBoundedOrder` `BoundedLatticeHom.instFunLike` `concreteCategory` `BoolAlg.instConcreteCategoryBoundedLatticeHomCarrier` `hasForgetToBoolAlg`	—	`CategoryTheory.InducedCategory.full`
`forgetToFinPartOrdFaithful` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `FinBoolAlg` `largeCategory` `FinPartOrd` `FinPartOrd.largeCategory` `CategoryTheory.forget₂` `BoundedLatticeHom` `BoolAlg.carrier` `toBoolAlg` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `BoolAlg.str` `BooleanAlgebra.toBoundedOrder` `BoundedLatticeHom.instFunLike` `concreteCategory` `OrderHom` `PartOrd.carrier` `FinPartOrd.toPartOrd` `PartialOrder.toPreorder` `FinPartOrd.instPartialOrderCarrier` `OrderHom.instFunLike` `FinPartOrd.concreteCategory` `hasForgetToFinPartOrd`	—	`CategoryTheory.ConcreteCategory.ext` `BoundedLatticeHom.ext` `CategoryTheory.congr_fun`
`hasForgetToFinPartOrd_forget₂_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `FinBoolAlg` `largeCategory` `FinPartOrd` `FinPartOrd.largeCategory` `CategoryTheory.HasForget₂.forget₂` `BoundedLatticeHom` `BoolAlg.carrier` `toBoolAlg` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `BoolAlg.str` `BooleanAlgebra.toBoundedOrder` `BoundedLatticeHom.instFunLike` `concreteCategory` `OrderHom` `PartOrd.carrier` `FinPartOrd.toPartOrd` `PartialOrder.toPreorder` `FinPartOrd.instPartialOrderCarrier` `OrderHom.instFunLike` `FinPartOrd.concreteCategory` `hasForgetToFinPartOrd` `CategoryTheory.InducedCategory.homMk` `PartOrd` `PartOrd.instCategory` `FinPartOrd.of` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `isFintype` `PartOrd.ofHom` `OrderHomClass.toOrderHom` `BoolAlg.Hom.hom` `CategoryTheory.InducedCategory.Hom.hom` `BoolAlg` `BoolAlg.instCategory`	—	—
`hasForgetToFinPartOrd_forget₂_obj_carrier` 📖	mathematical	—	`PartOrd.carrier` `FinPartOrd.toPartOrd` `CategoryTheory.Functor.obj` `FinBoolAlg` `largeCategory` `FinPartOrd` `FinPartOrd.largeCategory` `CategoryTheory.HasForget₂.forget₂` `BoundedLatticeHom` `BoolAlg.carrier` `toBoolAlg` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `BoolAlg.str` `BooleanAlgebra.toBoundedOrder` `BoundedLatticeHom.instFunLike` `concreteCategory` `OrderHom` `PartialOrder.toPreorder` `FinPartOrd.instPartialOrderCarrier` `OrderHom.instFunLike` `FinPartOrd.concreteCategory` `hasForgetToFinPartOrd`	—	—
`hasForgetToFinPartOrd_forget₂_obj_isFintype` 📖	mathematical	—	`FinPartOrd.isFintype` `CategoryTheory.Functor.obj` `FinBoolAlg` `largeCategory` `FinPartOrd` `FinPartOrd.largeCategory` `CategoryTheory.HasForget₂.forget₂` `BoundedLatticeHom` `BoolAlg.carrier` `toBoolAlg` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `BoolAlg.str` `BooleanAlgebra.toBoundedOrder` `BoundedLatticeHom.instFunLike` `concreteCategory` `OrderHom` `PartOrd.carrier` `FinPartOrd.toPartOrd` `PartialOrder.toPreorder` `FinPartOrd.instPartialOrderCarrier` `OrderHom.instFunLike` `FinPartOrd.concreteCategory` `hasForgetToFinPartOrd` `isFintype`	—	—
`hasForgetToFinPartOrd_forget₂_obj_str` 📖	mathematical	—	`PartOrd.str` `FinPartOrd.toPartOrd` `CategoryTheory.Functor.obj` `FinBoolAlg` `largeCategory` `FinPartOrd` `FinPartOrd.largeCategory` `CategoryTheory.HasForget₂.forget₂` `BoundedLatticeHom` `BoolAlg.carrier` `toBoolAlg` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `BoolAlg.str` `BooleanAlgebra.toBoundedOrder` `BoundedLatticeHom.instFunLike` `concreteCategory` `OrderHom` `PartOrd.carrier` `PartialOrder.toPreorder` `FinPartOrd.instPartialOrderCarrier` `OrderHom.instFunLike` `FinPartOrd.concreteCategory` `hasForgetToFinPartOrd` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf`	—	—

FinBoolAlg.Iso

Definitions

Name	Category	Theorems
`mk` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk_hom` 📖	mathematical	—	`CategoryTheory.Iso.hom` `FinBoolAlg` `FinBoolAlg.largeCategory` `CategoryTheory.InducedCategory.homMk` `BoolAlg` `BoolAlg.instCategory` `FinBoolAlg.toBoolAlg` `BoolAlg.ofHom` `BoolAlg.carrier` `BoolAlg.str`	—	—
`mk_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `FinBoolAlg` `FinBoolAlg.largeCategory` `CategoryTheory.InducedCategory.homMk` `BoolAlg` `BoolAlg.instCategory` `FinBoolAlg.toBoolAlg` `BoolAlg.ofHom` `BoolAlg.carrier` `BoolAlg.str`	—	—

(root)

Definitions

Name	Category	Theorems
`FinBoolAlg` 📖	CompData	15 math math: `FinBoolAlg.dualEquiv_inverse`, `FinBoolAlg.forgetToFinPartOrdFaithful`, `FinBoolAlg.dualEquiv_functor`, `fintypeToFinBoolAlgOp_map`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_carrier`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_isFintype`, `FinBoolAlg.Iso.mk_inv`, `finBoolAlg_dual_comp_forget_to_finBddDistLat`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_map`, `FinBoolAlg.forgetToBoolAlg_full`, `FinBoolAlg.Iso.mk_hom`, `FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_str`, `FinBoolAlg.dual_map`, `fintypeToFinBoolAlgOp_obj`, `FinBoolAlg.forgetToBoolAlgFaithful`
`fintypeToFinBoolAlgOp` 📖	CompOp	2 math math: `fintypeToFinBoolAlgOp_map`, `fintypeToFinBoolAlgOp_obj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finBoolAlg_dual_comp_forget_to_finBddDistLat` 📖	mathematical	—	`CategoryTheory.Functor.comp` `FinBoolAlg` `FinBoolAlg.largeCategory` `FinBddDistLat` `FinBddDistLat.instCategory` `FinBoolAlg.dual` `CategoryTheory.forget₂` `BoundedLatticeHom` `BoolAlg.carrier` `FinBoolAlg.toBoolAlg` `GeneralizedCoheytingAlgebra.toLattice` `CoheytingAlgebra.toGeneralizedCoheytingAlgebra` `BiheytingAlgebra.toCoheytingAlgebra` `BooleanAlgebra.toBiheytingAlgebra` `BoolAlg.str` `BooleanAlgebra.toBoundedOrder` `BoundedLatticeHom.instFunLike` `FinBoolAlg.concreteCategory` `DistLat.carrier` `BddDistLat.toDistLat` `FinBddDistLat.toBddDistLat` `DistribLattice.toLattice` `FinBddDistLat.instDistribLatticeCarrier` `FinBddDistLat.instBoundedOrderCarrier` `FinBddDistLat.instConcreteCategoryBoundedLatticeHomCarrier` `FinBoolAlg.hasForgetToFinBddDistLat` `FinBddDistLat.dual`	—	—
`fintypeToFinBoolAlgOp_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `FintypeCat` `FintypeCat.instCategory` `Opposite` `FinBoolAlg` `CategoryTheory.Category.opposite` `FinBoolAlg.largeCategory` `fintypeToFinBoolAlgOp` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `FinBoolAlg.of` `Set` `FintypeCat.carrier` `Set.instBooleanAlgebra` `Set.fintype` `FintypeCat.instFintypeCarrier` `CategoryTheory.InducedCategory.homMk` `BoolAlg` `BoolAlg.instCategory` `FinBoolAlg.toBoolAlg` `BoolAlg.ofHom`	—	—
`fintypeToFinBoolAlgOp_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `FintypeCat` `FintypeCat.instCategory` `Opposite` `FinBoolAlg` `CategoryTheory.Category.opposite` `FinBoolAlg.largeCategory` `fintypeToFinBoolAlgOp` `Opposite.op` `FinBoolAlg.of` `Set` `FintypeCat.carrier` `Set.instBooleanAlgebra` `Set.fintype` `FintypeCat.instFintypeCarrier`	—	—

---

← Back to Index