HeytAlg

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

Statistics

Metric	Count
Definitions HeytAlg, hom, hom, hom', mk, carrier, hasForgetToLat, instCategory, instCoeSortType, instConcreteCategoryHeytingHomCarrier, instInhabited, of, ofHom, str	14
Theorems ext, ext_iff, mk_hom, mk_inv, coe_comp, coe_id, coe_of, comp_apply, ext, ext_iff, forget_map, hasForgetToLat_forget₂_map, hasForgetToLat_forget₂_obj_carrier, hasForgetToLat_forget₂_obj_isBoundedOrder, hasForgetToLat_forget₂_obj_str, 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	27
Total	41

HeytAlg

Definitions

Name	Category	Theorems
carrier 📖	CompOp	21 math math: hasForgetToLat_forget₂_map, hom_id, Iso.mk_inv, hom_comp, hasForgetToLat_forget₂_obj_str, hasForgetToLat_forget₂_obj_carrier, coe_comp, BoolAlg.hasForgetToHeytAlg_forget₂_map, id_apply, coe_of, hom_inv_apply, inv_hom_apply, ofHom_hom, comp_apply, hasForgetToLat_forget₂_obj_isBoundedOrder, ofHom_apply, coe_id, BoolAlg.hasForgetToHeytAlg_forget₂_obj_coe, Iso.mk_hom, forget_map, ext_iff
hasForgetToLat 📖	CompOp	4 math math: hasForgetToLat_forget₂_map, hasForgetToLat_forget₂_obj_str, hasForgetToLat_forget₂_obj_carrier, hasForgetToLat_forget₂_obj_isBoundedOrder
instCategory 📖	CompOp	21 math math: hasForgetToLat_forget₂_map, hom_id, Iso.mk_inv, hom_comp, hasForgetToLat_forget₂_obj_str, hasForgetToLat_forget₂_obj_carrier, coe_comp, BoolAlg.hasForgetToHeytAlg_forget₂_map, id_apply, hom_inv_apply, inv_hom_apply, ofHom_id, comp_apply, hasForgetToLat_forget₂_obj_isBoundedOrder, ofHom_apply, ofHom_comp, coe_id, BoolAlg.hasForgetToHeytAlg_forget₂_obj_coe, Iso.mk_hom, forget_map, ext_iff
instCoeSortType 📖	CompOp	—
instConcreteCategoryHeytingHomCarrier 📖	CompOp	15 math math: hasForgetToLat_forget₂_map, hasForgetToLat_forget₂_obj_str, hasForgetToLat_forget₂_obj_carrier, coe_comp, BoolAlg.hasForgetToHeytAlg_forget₂_map, id_apply, hom_inv_apply, inv_hom_apply, comp_apply, hasForgetToLat_forget₂_obj_isBoundedOrder, ofHom_apply, coe_id, BoolAlg.hasForgetToHeytAlg_forget₂_obj_coe, forget_map, ext_iff
instInhabited 📖	CompOp	—
of 📖	CompOp	5 math math: coe_of, ofHom_id, hom_ofHom, ofHom_apply, ofHom_comp
ofHom 📖	CompOp	8 math math: Iso.mk_inv, BoolAlg.hasForgetToHeytAlg_forget₂_map, ofHom_id, ofHom_hom, hom_ofHom, ofHom_apply, ofHom_comp, Iso.mk_hom
str 📖	CompOp	20 math math: hasForgetToLat_forget₂_map, hom_id, Iso.mk_inv, hom_comp, hasForgetToLat_forget₂_obj_str, hasForgetToLat_forget₂_obj_carrier, coe_comp, BoolAlg.hasForgetToHeytAlg_forget₂_map, id_apply, hom_inv_apply, inv_hom_apply, ofHom_hom, comp_apply, hasForgetToLat_forget₂_obj_isBoundedOrder, ofHom_apply, coe_id, BoolAlg.hasForgetToHeytAlg_forget₂_obj_coe, Iso.mk_hom, forget_map, ext_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_comp 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom HeytAlg instCategory HeytingHom str HeytingHom.instFunLike instConcreteCategoryHeytingHomCarrier CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
coe_id 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom HeytAlg instCategory HeytingHom str HeytingHom.instFunLike instConcreteCategoryHeytingHomCarrier CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
coe_of 📖	mathematical	—	carrier of	—	—
comp_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom HeytAlg instCategory HeytingHom str HeytingHom.instFunLike instConcreteCategoryHeytingHomCarrier CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
ext 📖	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom HeytAlg instCategory HeytingHom str HeytingHom.instFunLike instConcreteCategoryHeytingHomCarrier	—	—	CategoryTheory.ConcreteCategory.hom_ext
ext_iff 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom HeytAlg instCategory HeytingHom str HeytingHom.instFunLike instConcreteCategoryHeytingHomCarrier	—	ext
forget_map 📖	mathematical	—	CategoryTheory.Functor.map HeytAlg instCategory CategoryTheory.types CategoryTheory.forget HeytingHom carrier str HeytingHom.instFunLike instConcreteCategoryHeytingHomCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom	—	—
hasForgetToLat_forget₂_map 📖	mathematical	—	CategoryTheory.Functor.map HeytAlg instCategory BddDistLat BddDistLat.instCategory CategoryTheory.HasForget₂.forget₂ HeytingHom carrier str HeytingHom.instFunLike instConcreteCategoryHeytingHomCarrier BoundedLatticeHom DistLat.carrier BddDistLat.toDistLat DistribLattice.toLattice BddDistLat.instDistribLatticeCarrier BddDistLat.isBoundedOrder BoundedLatticeHom.instFunLike BddDistLat.instConcreteCategoryBoundedLatticeHomCarrier hasForgetToLat BddDistLat.ofHom GeneralizedHeytingAlgebra.toDistribLattice HeytingAlgebra.toGeneralizedHeytingAlgebra HeytingAlgebra.toBoundedOrder	—	—
hasForgetToLat_forget₂_obj_carrier 📖	mathematical	—	DistLat.carrier BddDistLat.toDistLat CategoryTheory.Functor.obj HeytAlg instCategory BddDistLat BddDistLat.instCategory CategoryTheory.HasForget₂.forget₂ HeytingHom carrier str HeytingHom.instFunLike instConcreteCategoryHeytingHomCarrier BoundedLatticeHom DistribLattice.toLattice BddDistLat.instDistribLatticeCarrier BddDistLat.isBoundedOrder BoundedLatticeHom.instFunLike BddDistLat.instConcreteCategoryBoundedLatticeHomCarrier hasForgetToLat	—	—
hasForgetToLat_forget₂_obj_isBoundedOrder 📖	mathematical	—	BddDistLat.isBoundedOrder CategoryTheory.Functor.obj HeytAlg instCategory BddDistLat BddDistLat.instCategory CategoryTheory.HasForget₂.forget₂ HeytingHom carrier str HeytingHom.instFunLike instConcreteCategoryHeytingHomCarrier BoundedLatticeHom DistLat.carrier BddDistLat.toDistLat DistribLattice.toLattice BddDistLat.instDistribLatticeCarrier BoundedLatticeHom.instFunLike BddDistLat.instConcreteCategoryBoundedLatticeHomCarrier hasForgetToLat HeytingAlgebra.toBoundedOrder	—	—
hasForgetToLat_forget₂_obj_str 📖	mathematical	—	DistLat.str BddDistLat.toDistLat CategoryTheory.Functor.obj HeytAlg instCategory BddDistLat BddDistLat.instCategory CategoryTheory.HasForget₂.forget₂ HeytingHom carrier str HeytingHom.instFunLike instConcreteCategoryHeytingHomCarrier BoundedLatticeHom DistLat.carrier DistribLattice.toLattice BddDistLat.instDistribLatticeCarrier BddDistLat.isBoundedOrder BoundedLatticeHom.instFunLike BddDistLat.instConcreteCategoryBoundedLatticeHomCarrier hasForgetToLat GeneralizedHeytingAlgebra.toDistribLattice HeytingAlgebra.toGeneralizedHeytingAlgebra	—	—
hom_comp 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.comp HeytAlg CategoryTheory.Category.toCategoryStruct instCategory HeytingHom.comp carrier str	—	—
hom_ext 📖	—	Hom.hom	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.hom	—	hom_ext
hom_id 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.id HeytAlg CategoryTheory.Category.toCategoryStruct instCategory HeytingHom.id carrier str	—	—
hom_inv_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom HeytAlg instCategory HeytingHom str HeytingHom.instFunLike instConcreteCategoryHeytingHomCarrier 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 HeytAlg instCategory HeytingHom str HeytingHom.instFunLike instConcreteCategoryHeytingHomCarrier CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
inv_hom_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom HeytAlg instCategory HeytingHom str HeytingHom.instFunLike instConcreteCategoryHeytingHomCarrier CategoryTheory.Iso.inv CategoryTheory.Iso.hom	—	CategoryTheory.Iso.hom_inv_id_apply
ofHom_apply 📖	mathematical	—	DFunLike.coe of carrier CategoryTheory.ConcreteCategory.hom HeytAlg instCategory HeytingHom str HeytingHom.instFunLike instConcreteCategoryHeytingHomCarrier ofHom	—	—
ofHom_comp 📖	mathematical	—	ofHom HeytingHom.comp CategoryTheory.CategoryStruct.comp HeytAlg CategoryTheory.Category.toCategoryStruct instCategory of	—	—
ofHom_hom 📖	mathematical	—	ofHom carrier str Hom.hom	—	—
ofHom_id 📖	mathematical	—	ofHom HeytingHom.id CategoryTheory.CategoryStruct.id HeytAlg CategoryTheory.Category.toCategoryStruct instCategory of	—	—

HeytAlg.Hom

Definitions

Name	Category	Theorems
hom 📖	CompOp	5 math math: HeytAlg.hom_id, HeytAlg.hom_comp, HeytAlg.ofHom_hom, HeytAlg.hom_ofHom, HeytAlg.hom_ext_iff
hom' 📖	CompOp	1 math math: ext_iff

Theorems

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

HeytAlg.Hom.Simps

Definitions

Name	Category	Theorems
hom 📖	CompOp	—

HeytAlg.Iso

Definitions

Name	Category	Theorems
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_hom 📖	mathematical	—	CategoryTheory.Iso.hom HeytAlg HeytAlg.instCategory HeytAlg.ofHom HeytAlg.carrier HeytAlg.str GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra SemilatticeSup.toMax Lattice.toSemilatticeSup DFunLike.coe OrderIso Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instFunLikeOrderIso	—	—
mk_inv 📖	mathematical	—	CategoryTheory.Iso.inv HeytAlg HeytAlg.instCategory HeytAlg.ofHom HeytAlg.carrier HeytAlg.str GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra SemilatticeSup.toMax Lattice.toSemilatticeSup DFunLike.coe OrderIso Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instFunLikeOrderIso OrderIso.symm	—	—

(root)

Definitions

Name	Category	Theorems
HeytAlg 📖	CompData	21 math math: HeytAlg.hasForgetToLat_forget₂_map, HeytAlg.hom_id, HeytAlg.Iso.mk_inv, HeytAlg.hom_comp, HeytAlg.hasForgetToLat_forget₂_obj_str, HeytAlg.hasForgetToLat_forget₂_obj_carrier, HeytAlg.coe_comp, BoolAlg.hasForgetToHeytAlg_forget₂_map, HeytAlg.id_apply, HeytAlg.hom_inv_apply, HeytAlg.inv_hom_apply, HeytAlg.ofHom_id, HeytAlg.comp_apply, HeytAlg.hasForgetToLat_forget₂_obj_isBoundedOrder, HeytAlg.ofHom_apply, HeytAlg.ofHom_comp, HeytAlg.coe_id, BoolAlg.hasForgetToHeytAlg_forget₂_obj_coe, HeytAlg.Iso.mk_hom, HeytAlg.forget_map, HeytAlg.ext_iff

---

← Back to Index