BoolAlg

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

Statistics

Metric	Count
Definitions BoolAlg, hom, hom, hom', mk, carrier, dual, dualEquiv, hasForgetToBddDistLat, hasForgetToHeytAlg, instCategory, instCoeSortType, instConcreteCategoryBoundedLatticeHomCarrier, instInhabited, ofHom, str, toBddDistLat, typeToBoolAlgOp	18
Theorems ext, ext_iff, mk_hom, mk_inv, coe_comp, coe_id, coe_of, coe_toBddDistLat, comp_apply, dualEquiv_functor, dualEquiv_inverse, dual_map, ext, ext_iff, forget_map, hasForgetToHeytAlg_forget₂_map, hasForgetToHeytAlg_forget₂_obj_coe, hom_comp, hom_ext, hom_ext_iff, hom_id, hom_inv_apply, hom_ofHom, id_apply, inv_hom_apply, ofHom_apply, ofHom_comp, ofHom_hom, ofHom_id, boolAlg_dual_comp_forget_to_bddDistLat, typeToBoolAlgOp_map, typeToBoolAlgOp_obj	32
Total	50

BoolAlg

Definitions

Name	Category	Theorems
carrier 📖	CompOp	38 math math: coe_id, BoolRing.hasForgetToBoolAlg_forget₂_obj_coe, hasForgetToBoolRing_forget₂_obj_carrier, ext_iff, hasForgetToBoolRing_forget₂_map, boolRingCatEquivBoolAlg_functor, coe_toBddDistLat, hom_id, hasForgetToHeytAlg_forget₂_map, FinBoolAlg.coe_of, FinBoolAlg.forgetToFinPartOrdFaithful, coe_of, FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_carrier, hom_comp, dual_map, boolRingCatEquivBoolAlg_inverse, coe_comp, BoolRing.hasForgetToBoolAlg_forget₂_map, hom_inv_apply, FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_isFintype, FinBoolAlg.Iso.mk_inv, comp_apply, ofHom_hom, finBoolAlg_dual_comp_forget_to_finBddDistLat, Iso.mk_hom, hasForgetToHeytAlg_forget₂_obj_coe, inv_hom_apply, boolAlg_dual_comp_forget_to_bddDistLat, FinBoolAlg.hasForgetToFinPartOrd_forget₂_map, FinBoolAlg.forgetToBoolAlg_full, FinBoolAlg.Iso.mk_hom, FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_str, FinBoolAlg.dual_map, id_apply, FinBoolAlg.forgetToBoolAlgFaithful, Iso.mk_inv, ofHom_apply, forget_map
dual 📖	CompOp	4 math math: dualEquiv_functor, dual_map, dualEquiv_inverse, boolAlg_dual_comp_forget_to_bddDistLat
dualEquiv 📖	CompOp	2 math math: dualEquiv_functor, dualEquiv_inverse
hasForgetToBddDistLat 📖	CompOp	1 math math: boolAlg_dual_comp_forget_to_bddDistLat
hasForgetToHeytAlg 📖	CompOp	2 math math: hasForgetToHeytAlg_forget₂_map, hasForgetToHeytAlg_forget₂_obj_coe
instCategory 📖	CompOp	36 math math: coe_id, BoolRing.hasForgetToBoolAlg_forget₂_obj_coe, hasForgetToBoolRing_forget₂_obj_carrier, ext_iff, dualEquiv_functor, hasForgetToBoolRing_forget₂_map, boolRingCatEquivBoolAlg_functor, ofHom_comp, hom_id, hasForgetToHeytAlg_forget₂_map, fintypeToFinBoolAlgOp_map, typeToBoolAlgOp_map, hom_comp, ofHom_id, dual_map, dualEquiv_inverse, boolRingCatEquivBoolAlg_inverse, coe_comp, BoolRing.hasForgetToBoolAlg_forget₂_map, hom_inv_apply, FinBoolAlg.Iso.mk_inv, comp_apply, Iso.mk_hom, hasForgetToHeytAlg_forget₂_obj_coe, inv_hom_apply, boolAlg_dual_comp_forget_to_bddDistLat, FinBoolAlg.hasForgetToFinPartOrd_forget₂_map, FinBoolAlg.forgetToBoolAlg_full, FinBoolAlg.Iso.mk_hom, FinBoolAlg.dual_map, id_apply, FinBoolAlg.forgetToBoolAlgFaithful, Iso.mk_inv, ofHom_apply, forget_map, typeToBoolAlgOp_obj
instCoeSortType 📖	CompOp	—
instConcreteCategoryBoundedLatticeHomCarrier 📖	CompOp	20 math math: coe_id, BoolRing.hasForgetToBoolAlg_forget₂_obj_coe, hasForgetToBoolRing_forget₂_obj_carrier, ext_iff, hasForgetToBoolRing_forget₂_map, boolRingCatEquivBoolAlg_functor, hasForgetToHeytAlg_forget₂_map, boolRingCatEquivBoolAlg_inverse, coe_comp, BoolRing.hasForgetToBoolAlg_forget₂_map, hom_inv_apply, comp_apply, hasForgetToHeytAlg_forget₂_obj_coe, inv_hom_apply, boolAlg_dual_comp_forget_to_bddDistLat, FinBoolAlg.forgetToBoolAlg_full, id_apply, FinBoolAlg.forgetToBoolAlgFaithful, ofHom_apply, forget_map
instInhabited 📖	CompOp	—
ofHom 📖	CompOp	14 math math: ofHom_comp, fintypeToFinBoolAlgOp_map, typeToBoolAlgOp_map, ofHom_id, dual_map, BoolRing.hasForgetToBoolAlg_forget₂_map, hom_ofHom, FinBoolAlg.Iso.mk_inv, ofHom_hom, Iso.mk_hom, FinBoolAlg.Iso.mk_hom, FinBoolAlg.dual_map, Iso.mk_inv, ofHom_apply
str 📖	CompOp	35 math math: coe_id, BoolRing.hasForgetToBoolAlg_forget₂_obj_coe, hasForgetToBoolRing_forget₂_obj_carrier, ext_iff, hasForgetToBoolRing_forget₂_map, boolRingCatEquivBoolAlg_functor, hom_id, hasForgetToHeytAlg_forget₂_map, FinBoolAlg.forgetToFinPartOrdFaithful, FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_carrier, hom_comp, dual_map, boolRingCatEquivBoolAlg_inverse, coe_comp, BoolRing.hasForgetToBoolAlg_forget₂_map, hom_inv_apply, FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_isFintype, FinBoolAlg.Iso.mk_inv, comp_apply, ofHom_hom, finBoolAlg_dual_comp_forget_to_finBddDistLat, Iso.mk_hom, hasForgetToHeytAlg_forget₂_obj_coe, inv_hom_apply, boolAlg_dual_comp_forget_to_bddDistLat, FinBoolAlg.hasForgetToFinPartOrd_forget₂_map, FinBoolAlg.forgetToBoolAlg_full, FinBoolAlg.Iso.mk_hom, FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_str, FinBoolAlg.dual_map, id_apply, FinBoolAlg.forgetToBoolAlgFaithful, Iso.mk_inv, ofHom_apply, forget_map
toBddDistLat 📖	CompOp	1 math math: coe_toBddDistLat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_comp 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom BoolAlg instCategory BoundedLatticeHom GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra str BooleanAlgebra.toBoundedOrder BoundedLatticeHom.instFunLike instConcreteCategoryBoundedLatticeHomCarrier CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
coe_id 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom BoolAlg instCategory BoundedLatticeHom GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra str BooleanAlgebra.toBoundedOrder BoundedLatticeHom.instFunLike instConcreteCategoryBoundedLatticeHomCarrier CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
coe_of 📖	mathematical	—	carrier of	—	—
coe_toBddDistLat 📖	mathematical	—	DistLat.carrier BddDistLat.toDistLat toBddDistLat carrier	—	—
comp_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom BoolAlg instCategory BoundedLatticeHom GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra str BooleanAlgebra.toBoundedOrder BoundedLatticeHom.instFunLike instConcreteCategoryBoundedLatticeHomCarrier CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
dualEquiv_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor BoolAlg instCategory dualEquiv dual	—	—
dualEquiv_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse BoolAlg instCategory dualEquiv dual	—	—
dual_map 📖	mathematical	—	CategoryTheory.Functor.map BoolAlg instCategory dual ofHom OrderDual carrier OrderDual.instBooleanAlgebra str 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 Hom.hom	—	—
ext 📖	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom BoolAlg instCategory BoundedLatticeHom GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra str BooleanAlgebra.toBoundedOrder BoundedLatticeHom.instFunLike instConcreteCategoryBoundedLatticeHomCarrier	—	—	CategoryTheory.ConcreteCategory.hom_ext
ext_iff 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom BoolAlg instCategory BoundedLatticeHom GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra str BooleanAlgebra.toBoundedOrder BoundedLatticeHom.instFunLike instConcreteCategoryBoundedLatticeHomCarrier	—	ext
forget_map 📖	mathematical	—	CategoryTheory.Functor.map BoolAlg instCategory CategoryTheory.types CategoryTheory.forget BoundedLatticeHom carrier GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra str BooleanAlgebra.toBoundedOrder BoundedLatticeHom.instFunLike instConcreteCategoryBoundedLatticeHomCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom	—	—
hasForgetToHeytAlg_forget₂_map 📖	mathematical	—	CategoryTheory.Functor.map BoolAlg instCategory HeytAlg HeytAlg.instCategory CategoryTheory.HasForget₂.forget₂ BoundedLatticeHom carrier GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra str BooleanAlgebra.toBoundedOrder BoundedLatticeHom.instFunLike instConcreteCategoryBoundedLatticeHomCarrier HeytingHom HeytAlg.carrier HeytAlg.str HeytingHom.instFunLike HeytAlg.instConcreteCategoryHeytingHomCarrier hasForgetToHeytAlg HeytAlg.ofHom BiheytingAlgebra.toHeytingAlgebra GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra SemilatticeSup.toMax Lattice.toSemilatticeSup DFunLike.coe Hom.hom	—	—
hasForgetToHeytAlg_forget₂_obj_coe 📖	mathematical	—	HeytAlg.carrier CategoryTheory.Functor.obj BoolAlg instCategory HeytAlg HeytAlg.instCategory CategoryTheory.HasForget₂.forget₂ BoundedLatticeHom carrier GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra str BooleanAlgebra.toBoundedOrder BoundedLatticeHom.instFunLike instConcreteCategoryBoundedLatticeHomCarrier HeytingHom HeytAlg.str HeytingHom.instFunLike HeytAlg.instConcreteCategoryHeytingHomCarrier hasForgetToHeytAlg	—	—
hom_comp 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.comp BoolAlg CategoryTheory.Category.toCategoryStruct instCategory BoundedLatticeHom.comp carrier GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra str BooleanAlgebra.toBoundedOrder	—	—
hom_ext 📖	—	Hom.hom	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.hom	—	hom_ext
hom_id 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.id BoolAlg CategoryTheory.Category.toCategoryStruct instCategory BoundedLatticeHom.id carrier GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra str BooleanAlgebra.toBoundedOrder	—	—
hom_inv_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom BoolAlg instCategory BoundedLatticeHom GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra str BooleanAlgebra.toBoundedOrder BoundedLatticeHom.instFunLike instConcreteCategoryBoundedLatticeHomCarrier CategoryTheory.Iso.hom CategoryTheory.Iso.inv	—	CategoryTheory.Iso.inv_hom_id_apply
hom_ofHom 📖	mathematical	—	Hom.hom of ofHom	—	—
id_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom BoolAlg instCategory BoundedLatticeHom GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra str BooleanAlgebra.toBoundedOrder BoundedLatticeHom.instFunLike instConcreteCategoryBoundedLatticeHomCarrier CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
inv_hom_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom BoolAlg instCategory BoundedLatticeHom GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra str BooleanAlgebra.toBoundedOrder BoundedLatticeHom.instFunLike instConcreteCategoryBoundedLatticeHomCarrier CategoryTheory.Iso.inv CategoryTheory.Iso.hom	—	CategoryTheory.Iso.hom_inv_id_apply
ofHom_apply 📖	mathematical	—	DFunLike.coe of carrier CategoryTheory.ConcreteCategory.hom BoolAlg instCategory BoundedLatticeHom GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra str BooleanAlgebra.toBoundedOrder BoundedLatticeHom.instFunLike instConcreteCategoryBoundedLatticeHomCarrier ofHom	—	—
ofHom_comp 📖	mathematical	—	ofHom BoundedLatticeHom.comp GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra BooleanAlgebra.toBoundedOrder CategoryTheory.CategoryStruct.comp BoolAlg CategoryTheory.Category.toCategoryStruct instCategory of	—	—
ofHom_hom 📖	mathematical	—	ofHom carrier str Hom.hom	—	—
ofHom_id 📖	mathematical	—	ofHom BoundedLatticeHom.id GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra BooleanAlgebra.toBoundedOrder CategoryTheory.CategoryStruct.id BoolAlg CategoryTheory.Category.toCategoryStruct instCategory of	—	—

BoolAlg.Hom

Definitions

Name	Category	Theorems
hom 📖	CompOp	10 math math: BoolAlg.hasForgetToBoolRing_forget₂_map, BoolAlg.hom_id, BoolAlg.hasForgetToHeytAlg_forget₂_map, BoolAlg.hom_comp, BoolAlg.dual_map, BoolAlg.hom_ofHom, BoolAlg.ofHom_hom, BoolAlg.hom_ext_iff, FinBoolAlg.hasForgetToFinPartOrd_forget₂_map, FinBoolAlg.dual_map
hom' 📖	CompOp	1 math math: ext_iff

Theorems

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

BoolAlg.Hom.Simps

Definitions

Name	Category	Theorems
hom 📖	CompOp	—

BoolAlg.Iso

Definitions

Name	Category	Theorems
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_hom 📖	mathematical	—	CategoryTheory.Iso.hom BoolAlg BoolAlg.instCategory BoolAlg.ofHom BoolAlg.carrier BoolAlg.str	—	—
mk_inv 📖	mathematical	—	CategoryTheory.Iso.inv BoolAlg BoolAlg.instCategory BoolAlg.ofHom BoolAlg.carrier BoolAlg.str	—	—

(root)

Definitions

Name	Category	Theorems
BoolAlg 📖	CompData	36 math math: BoolAlg.coe_id, BoolRing.hasForgetToBoolAlg_forget₂_obj_coe, BoolAlg.hasForgetToBoolRing_forget₂_obj_carrier, BoolAlg.ext_iff, BoolAlg.dualEquiv_functor, BoolAlg.hasForgetToBoolRing_forget₂_map, boolRingCatEquivBoolAlg_functor, BoolAlg.ofHom_comp, BoolAlg.hom_id, BoolAlg.hasForgetToHeytAlg_forget₂_map, fintypeToFinBoolAlgOp_map, typeToBoolAlgOp_map, BoolAlg.hom_comp, BoolAlg.ofHom_id, BoolAlg.dual_map, BoolAlg.dualEquiv_inverse, boolRingCatEquivBoolAlg_inverse, BoolAlg.coe_comp, BoolRing.hasForgetToBoolAlg_forget₂_map, BoolAlg.hom_inv_apply, FinBoolAlg.Iso.mk_inv, BoolAlg.comp_apply, BoolAlg.Iso.mk_hom, BoolAlg.hasForgetToHeytAlg_forget₂_obj_coe, BoolAlg.inv_hom_apply, boolAlg_dual_comp_forget_to_bddDistLat, FinBoolAlg.hasForgetToFinPartOrd_forget₂_map, FinBoolAlg.forgetToBoolAlg_full, FinBoolAlg.Iso.mk_hom, FinBoolAlg.dual_map, BoolAlg.id_apply, FinBoolAlg.forgetToBoolAlgFaithful, BoolAlg.Iso.mk_inv, BoolAlg.ofHom_apply, BoolAlg.forget_map, typeToBoolAlgOp_obj
typeToBoolAlgOp 📖	CompOp	2 math math: typeToBoolAlgOp_map, typeToBoolAlgOp_obj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
boolAlg_dual_comp_forget_to_bddDistLat 📖	mathematical	—	CategoryTheory.Functor.comp BoolAlg BoolAlg.instCategory BddDistLat BddDistLat.instCategory BoolAlg.dual CategoryTheory.forget₂ BoundedLatticeHom BoolAlg.carrier GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra BiheytingAlgebra.toCoheytingAlgebra BooleanAlgebra.toBiheytingAlgebra BoolAlg.str BooleanAlgebra.toBoundedOrder BoundedLatticeHom.instFunLike BoolAlg.instConcreteCategoryBoundedLatticeHomCarrier DistLat.carrier BddDistLat.toDistLat DistribLattice.toLattice BddDistLat.instDistribLatticeCarrier BddDistLat.isBoundedOrder BddDistLat.instConcreteCategoryBoundedLatticeHomCarrier BoolAlg.hasForgetToBddDistLat BddDistLat.dual	—	—
typeToBoolAlgOp_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.types Opposite BoolAlg CategoryTheory.Category.opposite BoolAlg.instCategory typeToBoolAlgOp Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct BoolAlg.of Set Set.instBooleanAlgebra BoolAlg.ofHom	—	—
typeToBoolAlgOp_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.types Opposite BoolAlg CategoryTheory.Category.opposite BoolAlg.instCategory typeToBoolAlgOp Opposite.op BoolAlg.of Set Set.instBooleanAlgebra	—	—

---

← Back to Index