Lat

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

Statistics

Metric	Count
Definitions Lat, hom, hom, hom', mk, carrier, dual, dualEquiv, hasForgetToPartOrd, 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, Lat_dual_comp_forget_to_partOrd	27
Total	42

Lat

Definitions

Name	Category	Theorems
carrier 📖	CompOp	44 math math: ext_iff, BddLat.hom_comp, dual_map, coe_id, hom_comp, forget_map, bddLat_dual_comp_forget_to_lat, coe_of, BddLat.forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd, comp_apply, distLat_dual_comp_forget_to_Lat, BddDistLat.coe_toBddLat, Iso.mk_inv, BddLat.forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd, BddLat.coe_of, bddLat_dual_comp_forget_to_semilatSupCat, ofHom_apply, bddLat_dual_comp_forget_to_semilatInfCat, bddLat_dual_comp_forget_to_bddOrd, BddLat.forget_lat_partOrd_eq_forget_bddOrd_partOrd, BddLat.coe_forget_to_lat, BddDistLat.forget_bddLat_lat_eq_forget_distLat_lat, hom_id, Lat_dual_comp_forget_to_partOrd, BddLat.Iso.mk_hom, completeLat_dual_comp_forget_to_bddLat, BddLat.coe_forget_to_semilatSup, hom_inv_apply, BddLat.comp_apply, SimplexCategory.toCat_obj, id_apply, BddLat.id_apply, BddLat.coe_forget_to_bddOrd, BddLat.coe_forget_to_semilatInf, inv_hom_apply, Iso.mk_hom, BddLat.ext_iff, BddLat.hom_id, linOrd_dual_comp_forget_to_Lat, SimplexCategory.toCat_map, BddLat.dual_map, ofHom_hom, coe_comp, BddLat.Iso.mk_inv
dual 📖	CompOp	7 math math: dual_map, bddLat_dual_comp_forget_to_lat, dualEquiv_functor, distLat_dual_comp_forget_to_Lat, dualEquiv_inverse, Lat_dual_comp_forget_to_partOrd, linOrd_dual_comp_forget_to_Lat
dualEquiv 📖	CompOp	2 math math: dualEquiv_functor, dualEquiv_inverse
hasForgetToPartOrd 📖	CompOp	4 math math: BddLat.forget_lat_partOrd_eq_forget_bddOrd_partOrd, Lat_dual_comp_forget_to_partOrd, SimplexCategory.toCat_obj, SimplexCategory.toCat_map
instCategory 📖	CompOp	31 math math: ext_iff, BddLat.hom_comp, dual_map, coe_id, hom_comp, forget_map, bddLat_dual_comp_forget_to_lat, comp_apply, dualEquiv_functor, distLat_dual_comp_forget_to_Lat, Iso.mk_inv, ofHom_apply, dualEquiv_inverse, BddLat.forget_lat_partOrd_eq_forget_bddOrd_partOrd, BddLat.coe_forget_to_lat, BddDistLat.forget_bddLat_lat_eq_forget_distLat_lat, hom_id, Lat_dual_comp_forget_to_partOrd, hom_inv_apply, BddLat.comp_apply, SimplexCategory.toCat_obj, id_apply, BddLat.id_apply, ofHom_comp, inv_hom_apply, Iso.mk_hom, BddLat.hom_id, linOrd_dual_comp_forget_to_Lat, SimplexCategory.toCat_map, ofHom_id, coe_comp
instCoeSortType 📖	CompOp	—
instConcreteCategoryLatticeHomCarrier 📖	CompOp	20 math math: ext_iff, coe_id, forget_map, bddLat_dual_comp_forget_to_lat, comp_apply, distLat_dual_comp_forget_to_Lat, ofHom_apply, BddLat.forget_lat_partOrd_eq_forget_bddOrd_partOrd, BddLat.coe_forget_to_lat, BddDistLat.forget_bddLat_lat_eq_forget_distLat_lat, Lat_dual_comp_forget_to_partOrd, hom_inv_apply, BddLat.comp_apply, SimplexCategory.toCat_obj, id_apply, BddLat.id_apply, inv_hom_apply, linOrd_dual_comp_forget_to_Lat, SimplexCategory.toCat_map, coe_comp
of 📖	CompOp	5 math math: coe_of, ofHom_apply, hom_ofHom, ofHom_comp, ofHom_id
ofHom 📖	CompOp	8 math math: dual_map, Iso.mk_inv, ofHom_apply, hom_ofHom, ofHom_comp, Iso.mk_hom, ofHom_hom, ofHom_id
str 📖	CompOp	41 math math: ext_iff, BddLat.hom_comp, dual_map, coe_id, hom_comp, forget_map, bddLat_dual_comp_forget_to_lat, BddLat.forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd, comp_apply, distLat_dual_comp_forget_to_Lat, Iso.mk_inv, BddLat.forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd, bddLat_dual_comp_forget_to_semilatSupCat, ofHom_apply, bddLat_dual_comp_forget_to_semilatInfCat, bddLat_dual_comp_forget_to_bddOrd, BddLat.forget_lat_partOrd_eq_forget_bddOrd_partOrd, BddLat.coe_forget_to_lat, BddDistLat.forget_bddLat_lat_eq_forget_distLat_lat, hom_id, Lat_dual_comp_forget_to_partOrd, BddLat.Iso.mk_hom, completeLat_dual_comp_forget_to_bddLat, BddLat.coe_forget_to_semilatSup, hom_inv_apply, BddLat.comp_apply, SimplexCategory.toCat_obj, id_apply, BddLat.id_apply, BddLat.coe_forget_to_bddOrd, BddLat.coe_forget_to_semilatInf, inv_hom_apply, Iso.mk_hom, BddLat.ext_iff, BddLat.hom_id, linOrd_dual_comp_forget_to_Lat, SimplexCategory.toCat_map, BddLat.dual_map, ofHom_hom, coe_comp, BddLat.Iso.mk_inv

Theorems

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

Lat.Hom

Definitions

Name	Category	Theorems
hom 📖	CompOp	8 math math: BddLat.hom_comp, Lat.hom_ext_iff, Lat.dual_map, Lat.hom_comp, Lat.hom_ofHom, Lat.hom_id, BddLat.hom_id, Lat.ofHom_hom
hom' 📖	CompOp	1 math math: ext_iff

Theorems

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

Lat.Hom.Simps

Definitions

Name	Category	Theorems
hom 📖	CompOp	—

Lat.Iso

Definitions

Name	Category	Theorems
mk 📖	CompOp	—

Theorems

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

(root)

Definitions

Name	Category	Theorems
Lat 📖	CompData	31 math math: Lat.ext_iff, BddLat.hom_comp, Lat.dual_map, Lat.coe_id, Lat.hom_comp, Lat.forget_map, bddLat_dual_comp_forget_to_lat, Lat.comp_apply, Lat.dualEquiv_functor, distLat_dual_comp_forget_to_Lat, Lat.Iso.mk_inv, Lat.ofHom_apply, Lat.dualEquiv_inverse, BddLat.forget_lat_partOrd_eq_forget_bddOrd_partOrd, BddLat.coe_forget_to_lat, BddDistLat.forget_bddLat_lat_eq_forget_distLat_lat, Lat.hom_id, Lat_dual_comp_forget_to_partOrd, Lat.hom_inv_apply, BddLat.comp_apply, SimplexCategory.toCat_obj, Lat.id_apply, BddLat.id_apply, Lat.ofHom_comp, Lat.inv_hom_apply, Lat.Iso.mk_hom, BddLat.hom_id, linOrd_dual_comp_forget_to_Lat, SimplexCategory.toCat_map, Lat.ofHom_id, Lat.coe_comp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Lat_dual_comp_forget_to_partOrd 📖	mathematical	—	CategoryTheory.Functor.comp Lat Lat.instCategory PartOrd PartOrd.instCategory Lat.dual CategoryTheory.forget₂ LatticeHom Lat.carrier Lat.str LatticeHom.instFunLike Lat.instConcreteCategoryLatticeHomCarrier OrderHom PartOrd.carrier PartialOrder.toPreorder PartOrd.str OrderHom.instFunLike PartOrd.instConcreteCategoryOrderHomCarrier Lat.hasForgetToPartOrd PartOrd.dual	—	—

---

← Back to Index