Frm

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

Statistics

Metric	Count
Definitions hom, hom, hom', mk, carrier, hasForgetToLat, instCategory, instCoeSortType, instConcreteCategoryFrameHomCarrier, instInhabited, ofHom, str	12
Theorems ext, ext_iff, mk_hom, mk_inv, coe_comp, coe_id, coe_of, comp_apply, 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	23
Total	35

Frm

Definitions

Name	Category	Theorems
carrier 📖	CompOp	17 math math: coe_comp, Iso.mk_hom, coe_of, ext_iff, Locale.coe_of, Iso.mk_inv, ofHom_hom, hom_comp, id_apply, coe_id, inv_hom_apply, topCatOpToFrm_obj_coe, hom_inv_apply, hom_id, ofHom_apply, comp_apply, forget_map
hasForgetToLat 📖	CompOp	—
instCategory 📖	CompOp	20 math math: coe_comp, Iso.mk_hom, topCatOpToFrm_map, ext_iff, Iso.mk_inv, topToLocale_obj, hom_comp, id_apply, coe_id, inv_hom_apply, CompHausOpToFrame.faithful, topCatOpToFrm_obj_coe, hom_inv_apply, topToLocale_map, ofHom_comp, ofHom_id, hom_id, ofHom_apply, comp_apply, forget_map
instCoeSortType 📖	CompOp	—
instConcreteCategoryFrameHomCarrier 📖	CompOp	9 math math: coe_comp, ext_iff, id_apply, coe_id, inv_hom_apply, hom_inv_apply, ofHom_apply, comp_apply, forget_map
instInhabited 📖	CompOp	—
ofHom 📖	CompOp	9 math math: Iso.mk_hom, topCatOpToFrm_map, Iso.mk_inv, ofHom_hom, hom_ofHom, topToLocale_map, ofHom_comp, ofHom_id, ofHom_apply
str 📖	CompOp	14 math math: coe_comp, Iso.mk_hom, ext_iff, Iso.mk_inv, ofHom_hom, hom_comp, id_apply, coe_id, inv_hom_apply, hom_inv_apply, hom_id, ofHom_apply, comp_apply, forget_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_comp 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom Frm instCategory FrameHom Order.Frame.toCompleteLattice str FrameHom.instFunLike instConcreteCategoryFrameHomCarrier CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
coe_id 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom Frm instCategory FrameHom Order.Frame.toCompleteLattice str FrameHom.instFunLike instConcreteCategoryFrameHomCarrier CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
coe_of 📖	mathematical	—	carrier of	—	—
comp_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom Frm instCategory FrameHom Order.Frame.toCompleteLattice str FrameHom.instFunLike instConcreteCategoryFrameHomCarrier CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
ext 📖	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom Frm instCategory FrameHom Order.Frame.toCompleteLattice str FrameHom.instFunLike instConcreteCategoryFrameHomCarrier	—	—	CategoryTheory.ConcreteCategory.hom_ext
ext_iff 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom Frm instCategory FrameHom Order.Frame.toCompleteLattice str FrameHom.instFunLike instConcreteCategoryFrameHomCarrier	—	ext
forget_map 📖	mathematical	—	CategoryTheory.Functor.map Frm instCategory CategoryTheory.types CategoryTheory.forget FrameHom carrier Order.Frame.toCompleteLattice str FrameHom.instFunLike instConcreteCategoryFrameHomCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom	—	—
hom_comp 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.comp Frm CategoryTheory.Category.toCategoryStruct instCategory FrameHom.comp carrier Order.Frame.toCompleteLattice str	—	—
hom_ext 📖	—	Hom.hom	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.hom	—	hom_ext
hom_id 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.id Frm CategoryTheory.Category.toCategoryStruct instCategory FrameHom.id carrier Order.Frame.toCompleteLattice str	—	—
hom_inv_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom Frm instCategory FrameHom Order.Frame.toCompleteLattice str FrameHom.instFunLike instConcreteCategoryFrameHomCarrier 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 Frm instCategory FrameHom Order.Frame.toCompleteLattice str FrameHom.instFunLike instConcreteCategoryFrameHomCarrier CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
inv_hom_apply 📖	mathematical	—	DFunLike.coe carrier CategoryTheory.ConcreteCategory.hom Frm instCategory FrameHom Order.Frame.toCompleteLattice str FrameHom.instFunLike instConcreteCategoryFrameHomCarrier CategoryTheory.Iso.inv CategoryTheory.Iso.hom	—	CategoryTheory.Iso.hom_inv_id_apply
ofHom_apply 📖	mathematical	—	DFunLike.coe of carrier CategoryTheory.ConcreteCategory.hom Frm instCategory FrameHom Order.Frame.toCompleteLattice str FrameHom.instFunLike instConcreteCategoryFrameHomCarrier ofHom	—	—
ofHom_comp 📖	mathematical	—	ofHom FrameHom.comp Order.Frame.toCompleteLattice CategoryTheory.CategoryStruct.comp Frm CategoryTheory.Category.toCategoryStruct instCategory of	—	—
ofHom_hom 📖	mathematical	—	ofHom carrier str Hom.hom	—	—
ofHom_id 📖	mathematical	—	ofHom FrameHom.id Order.Frame.toCompleteLattice CategoryTheory.CategoryStruct.id Frm CategoryTheory.Category.toCategoryStruct instCategory of	—	—

Frm.Hom

Definitions

Name	Category	Theorems
hom 📖	CompOp	5 math math: Frm.ofHom_hom, Frm.hom_comp, Frm.hom_ofHom, Frm.hom_id, Frm.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

Frm.Hom.Simps

Definitions

Name	Category	Theorems
hom 📖	CompOp	—

Frm.Iso

Definitions

Name	Category	Theorems
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_hom 📖	mathematical	—	CategoryTheory.Iso.hom Frm Frm.instCategory Frm.ofHom Frm.carrier Frm.str Order.Frame.toCompleteLattice SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder DFunLike.coe OrderIso CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf instFunLikeOrderIso	—	—
mk_inv 📖	mathematical	—	CategoryTheory.Iso.inv Frm Frm.instCategory Frm.ofHom Frm.carrier Frm.str Order.Frame.toCompleteLattice SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder DFunLike.coe OrderIso CompleteSemilatticeInf.toPartialOrder CompleteLattice.toCompleteSemilatticeInf instFunLikeOrderIso OrderIso.symm	—	—

---

← Back to Index