DistLat

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

Statistics

Metric	Count
Definitions DistLat, hom, hom, hom', mk, carrier, dual, dualEquiv, hasForgetToLat, instCategory, instCoeSortType, instConcreteCategoryLatticeHomCarrier, of, ofHom, str	15
Theorems ext, ext_iff, mk_hom, mk_inv, coe_comp, coe_id, coe_of, comp_apply, dualEquiv_functor, dualEquiv_inverse, dual_map, ext, ext_iff, forget_map, 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, distLat_dual_comp_forget_to_Lat	27
Total	42

DistLat

Definitions

Name	Category	Theorems
carrier 📖	CompOp	59 math math: hom_inv_apply, HeytAlg.hasForgetToLat_forget₂_map, BddDistLat.ofHom_hom, dual_map, FinBddDistLat.ofHom_apply, BddDistLat.hom_id, BddDistLat.coe_id, HeytAlg.hasForgetToLat_forget₂_obj_str, FinBddDistLat.hom_inv_apply, HeytAlg.hasForgetToLat_forget₂_obj_carrier, ofHom_hom, FinBddDistLat.ext_iff, BoolAlg.coe_toBddDistLat, ext_iff, Iso.mk_inv, FinBddDistLat.coe_id, FinBddDistLat.inv_hom_apply, hom_id, finBddDistLat_dual_comp_forget_to_bddDistLat, distLat_dual_comp_forget_to_Lat, FinBddDistLat.forget_map, forget_map, BddDistLat.coe_comp, BddDistLat.coe_toBddLat, id_apply, BddDistLat.forget_map, FinBddDistLat.comp_apply, BddDistLat.dual_map, BddDistLat.inv_hom_apply, ofHom_apply, BddDistLat.Iso.mk_hom, BddDistLat.ofHom_apply, HeytAlg.hasForgetToLat_forget₂_obj_isBoundedOrder, FinBddDistLat.ofHom_hom, BddDistLat.id_apply, BddDistLat.forget_bddLat_lat_eq_forget_distLat_lat, finBoolAlg_dual_comp_forget_to_finBddDistLat, FinBddDistLat.hom_comp, coe_of, coe_id, FinBddDistLat.coe_comp, FinBddDistLat.Iso.mk_inv, BddDistLat.coe_of, coe_comp, BddDistLat.ext_iff, Iso.mk_hom, boolAlg_dual_comp_forget_to_bddDistLat, FinBddDistLat.id_apply, BddDistLat.comp_apply, BddDistLat.hom_comp, bddDistLat_dual_comp_forget_to_distLat, comp_apply, FinBddDistLat.hom_id, FinBddDistLat.dual_map, hom_comp, inv_hom_apply, BddDistLat.Iso.mk_inv, FinBddDistLat.Iso.mk_hom, BddDistLat.hom_inv_apply
dual 📖	CompOp	5 math math: dual_map, distLat_dual_comp_forget_to_Lat, dualEquiv_functor, bddDistLat_dual_comp_forget_to_distLat, dualEquiv_inverse
dualEquiv 📖	CompOp	2 math math: dualEquiv_functor, dualEquiv_inverse
hasForgetToLat 📖	CompOp	2 math math: distLat_dual_comp_forget_to_Lat, BddDistLat.forget_bddLat_lat_eq_forget_distLat_lat
instCategory 📖	CompOp	21 math math: hom_inv_apply, dual_map, ext_iff, Iso.mk_inv, hom_id, distLat_dual_comp_forget_to_Lat, forget_map, dualEquiv_functor, id_apply, ofHom_apply, BddDistLat.forget_bddLat_lat_eq_forget_distLat_lat, ofHom_id, coe_id, coe_comp, Iso.mk_hom, bddDistLat_dual_comp_forget_to_distLat, comp_apply, hom_comp, inv_hom_apply, dualEquiv_inverse, ofHom_comp
instCoeSortType 📖	CompOp	—
instConcreteCategoryLatticeHomCarrier 📖	CompOp	12 math math: hom_inv_apply, ext_iff, distLat_dual_comp_forget_to_Lat, forget_map, id_apply, ofHom_apply, BddDistLat.forget_bddLat_lat_eq_forget_distLat_lat, coe_id, coe_comp, bddDistLat_dual_comp_forget_to_distLat, comp_apply, inv_hom_apply
of 📖	CompOp	5 math math: hom_ofHom, ofHom_apply, coe_of, ofHom_id, ofHom_comp
ofHom 📖	CompOp	8 math math: dual_map, ofHom_hom, Iso.mk_inv, hom_ofHom, ofHom_apply, ofHom_id, Iso.mk_hom, ofHom_comp
str 📖	CompOp	23 math math: hom_inv_apply, dual_map, HeytAlg.hasForgetToLat_forget₂_obj_str, ofHom_hom, ext_iff, Iso.mk_inv, hom_id, distLat_dual_comp_forget_to_Lat, forget_map, id_apply, ofHom_apply, BddDistLat.Iso.mk_hom, BddDistLat.forget_bddLat_lat_eq_forget_distLat_lat, coe_id, FinBddDistLat.Iso.mk_inv, coe_comp, Iso.mk_hom, bddDistLat_dual_comp_forget_to_distLat, comp_apply, hom_comp, inv_hom_apply, BddDistLat.Iso.mk_inv, FinBddDistLat.Iso.mk_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_comp 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom DistLat instCategory LatticeHom DistribLattice.toLattice str LatticeHom.instFunLike instConcreteCategoryLatticeHomCarrier CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
coe_id 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom DistLat instCategory LatticeHom DistribLattice.toLattice str LatticeHom.instFunLike instConcreteCategoryLatticeHomCarrier CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
coe_of 📖	mathematical	—	carrier of	—	—
comp_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom DistLat instCategory LatticeHom DistribLattice.toLattice str LatticeHom.instFunLike instConcreteCategoryLatticeHomCarrier CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
dualEquiv_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor DistLat instCategory dualEquiv dual	—	—
dualEquiv_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse DistLat instCategory dualEquiv dual	—	—
dual_map 📖	mathematical	—	CategoryTheory.Functor.map DistLat instCategory dual ofHom OrderDual carrier OrderDual.instDistribLattice str DFunLike.coe Equiv LatticeHom DistribLattice.toLattice OrderDual.instLattice EquivLike.toFunLike Equiv.instEquivLike LatticeHom.dual Hom.hom	—	—
ext 📖	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom DistLat instCategory LatticeHom DistribLattice.toLattice str LatticeHom.instFunLike instConcreteCategoryLatticeHomCarrier	—	—	CategoryTheory.ConcreteCategory.hom_ext
ext_iff 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom DistLat instCategory LatticeHom DistribLattice.toLattice str LatticeHom.instFunLike instConcreteCategoryLatticeHomCarrier	—	ext
forget_map 📖	mathematical	—	CategoryTheory.Functor.map DistLat instCategory CategoryTheory.types CategoryTheory.forget LatticeHom carrier DistribLattice.toLattice str LatticeHom.instFunLike instConcreteCategoryLatticeHomCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom	—	—
hom_comp 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.comp DistLat CategoryTheory.Category.toCategoryStruct instCategory LatticeHom.comp carrier DistribLattice.toLattice str	—	—
hom_ext 📖	—	Hom.hom	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.hom	—	hom_ext
hom_id 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.id DistLat CategoryTheory.Category.toCategoryStruct instCategory LatticeHom.id carrier DistribLattice.toLattice str	—	—
hom_inv_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom DistLat instCategory LatticeHom DistribLattice.toLattice str LatticeHom.instFunLike instConcreteCategoryLatticeHomCarrier 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 DistLat instCategory LatticeHom DistribLattice.toLattice str LatticeHom.instFunLike instConcreteCategoryLatticeHomCarrier CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
inv_hom_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom DistLat instCategory LatticeHom DistribLattice.toLattice str LatticeHom.instFunLike instConcreteCategoryLatticeHomCarrier CategoryTheory.Iso.inv CategoryTheory.Iso.hom	—	CategoryTheory.Iso.hom_inv_id_apply
ofHom_apply 📖	mathematical	—	DFunLike.coe of carrier CategoryTheory.ConcreteCategory.hom DistLat instCategory LatticeHom DistribLattice.toLattice str LatticeHom.instFunLike instConcreteCategoryLatticeHomCarrier ofHom	—	—
ofHom_comp 📖	mathematical	—	ofHom LatticeHom.comp DistribLattice.toLattice CategoryTheory.CategoryStruct.comp DistLat CategoryTheory.Category.toCategoryStruct instCategory of	—	—
ofHom_hom 📖	mathematical	—	ofHom carrier str Hom.hom	—	—
ofHom_id 📖	mathematical	—	ofHom LatticeHom.id DistribLattice.toLattice CategoryTheory.CategoryStruct.id DistLat CategoryTheory.Category.toCategoryStruct instCategory of	—	—

DistLat.Hom

Definitions

Name	Category	Theorems
hom 📖	CompOp	6 math math: DistLat.dual_map, DistLat.ofHom_hom, DistLat.hom_ext_iff, DistLat.hom_id, DistLat.hom_ofHom, DistLat.hom_comp
hom' 📖	CompOp	1 math math: ext_iff

Theorems

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

DistLat.Hom.Simps

Definitions

Name	Category	Theorems
hom 📖	CompOp	—

DistLat.Iso

Definitions

Name	Category	Theorems
mk 📖	CompOp	—

Theorems

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

(root)

Definitions

Name	Category	Theorems
DistLat 📖	CompData	21 math math: DistLat.hom_inv_apply, DistLat.dual_map, DistLat.ext_iff, DistLat.Iso.mk_inv, DistLat.hom_id, distLat_dual_comp_forget_to_Lat, DistLat.forget_map, DistLat.dualEquiv_functor, DistLat.id_apply, DistLat.ofHom_apply, BddDistLat.forget_bddLat_lat_eq_forget_distLat_lat, DistLat.ofHom_id, DistLat.coe_id, DistLat.coe_comp, DistLat.Iso.mk_hom, bddDistLat_dual_comp_forget_to_distLat, DistLat.comp_apply, DistLat.hom_comp, DistLat.inv_hom_apply, DistLat.dualEquiv_inverse, DistLat.ofHom_comp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
distLat_dual_comp_forget_to_Lat 📖	mathematical	—	CategoryTheory.Functor.comp DistLat DistLat.instCategory Lat Lat.instCategory DistLat.dual CategoryTheory.forget₂ LatticeHom DistLat.carrier DistribLattice.toLattice DistLat.str LatticeHom.instFunLike DistLat.instConcreteCategoryLatticeHomCarrier Lat.carrier Lat.str Lat.instConcreteCategoryLatticeHomCarrier DistLat.hasForgetToLat Lat.dual	—	—

---

← Back to Index