Preord

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

Statistics

Metric	Count
Definitions Preord, hom, hom, hom', mk, carrier, dual, dualEquiv, instCategory, instCoeSortType, instConcreteCategoryOrderHomCarrier, instInhabited, ofHom, str, preordToCat	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, instFaithfulPreordCatPreordToCat, instFullPreordCatPreordToCat, preordToCat_map, preordToCat_obj	30
Total	45

Preord

Definitions

Name	Category	Theorems
carrier 📖	CompOp	30 math math: alexDiscEquivPreord_inverse_obj_carrier, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe, coe_id, ext_iff, inv_hom_apply, hom_inv_apply, alexDiscEquivPreord_inverse_obj_str, ofHom_apply, alexDiscEquivPreord_inverse_map, id_apply, hom_id, coe_of, forget_map, hom_comp, Iso.mk_hom, dual_map, alexDiscEquivPreord_unitIso, coe_comp, preordToCat_obj, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe', preordToCat_map, topToPreord_obj_coe, SimplexCategory.toCat_obj, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_hom_app_hom_coe, Iso.mk_inv, alexDiscEquivPreord_counitIso, comp_apply, SimplexCategory.toCat_map, ofHom_hom, partOrd_dual_comp_forget_to_preord
dual 📖	CompOp	7 math math: preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe, dualEquiv_inverse, dualEquiv_functor, dual_map, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe', preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_hom_app_hom_coe, partOrd_dual_comp_forget_to_preord
dualEquiv 📖	CompOp	2 math math: dualEquiv_inverse, dualEquiv_functor
instCategory 📖	CompOp	36 math math: ofHom_id, alexDiscEquivPreord_inverse_obj_carrier, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe, coe_id, ext_iff, inv_hom_apply, hom_inv_apply, alexDiscEquivPreord_inverse_obj_str, ofHom_apply, dualEquiv_inverse, alexDiscEquivPreord_inverse_map, instFaithfulPreordCatPreordToCat, id_apply, hom_id, dualEquiv_functor, forget_map, instFullPreordCatPreordToCat, hom_comp, Iso.mk_hom, dual_map, alexDiscEquivPreord_unitIso, coe_comp, topToPreord_map, preordToCat_obj, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe', preordToCat_map, topToPreord_obj_coe, SimplexCategory.toCat_obj, ofHom_comp, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_hom_app_hom_coe, Iso.mk_inv, alexDiscEquivPreord_counitIso, comp_apply, SimplexCategory.toCat_map, partOrd_dual_comp_forget_to_preord, alexDiscEquivPreord_functor
instCoeSortType 📖	CompOp	—
instConcreteCategoryOrderHomCarrier 📖	CompOp	12 math math: coe_id, ext_iff, inv_hom_apply, hom_inv_apply, ofHom_apply, id_apply, forget_map, coe_comp, SimplexCategory.toCat_obj, comp_apply, SimplexCategory.toCat_map, partOrd_dual_comp_forget_to_preord
instInhabited 📖	CompOp	—
ofHom 📖	CompOp	9 math math: ofHom_id, hom_ofHom, ofHom_apply, Iso.mk_hom, dual_map, topToPreord_map, ofHom_comp, Iso.mk_inv, ofHom_hom
str 📖	CompOp	27 math math: preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe, coe_id, ext_iff, inv_hom_apply, hom_inv_apply, alexDiscEquivPreord_inverse_obj_str, ofHom_apply, alexDiscEquivPreord_inverse_map, id_apply, hom_id, forget_map, hom_comp, Iso.mk_hom, dual_map, alexDiscEquivPreord_unitIso, coe_comp, preordToCat_obj, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe', preordToCat_map, SimplexCategory.toCat_obj, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_hom_app_hom_coe, Iso.mk_inv, alexDiscEquivPreord_counitIso, comp_apply, SimplexCategory.toCat_map, ofHom_hom, partOrd_dual_comp_forget_to_preord

Theorems

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

Preord.Hom

Definitions

Name	Category	Theorems
hom 📖	CompOp	11 math math: Preord.hom_ofHom, alexDiscEquivPreord_inverse_map, Preord.hom_id, Preord.hom_comp, Preord.dual_map, alexDiscEquivPreord_unitIso, preordToCat_map, alexDiscEquivPreord_counitIso, SimplexCategory.toCat_map, Preord.ofHom_hom, Preord.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

Preord.Hom.Simps

Definitions

Name	Category	Theorems
hom 📖	CompOp	—

Preord.Iso

Definitions

Name	Category	Theorems
mk 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_hom 📖	mathematical	—	CategoryTheory.Iso.hom Preord Preord.instCategory Preord.ofHom Preord.carrier Preord.str OrderHomClass.toOrderHom OrderIso Preorder.toLE instFunLikeOrderIso	—	—
mk_inv 📖	mathematical	—	CategoryTheory.Iso.inv Preord Preord.instCategory Preord.ofHom Preord.carrier Preord.str OrderHomClass.toOrderHom OrderIso Preorder.toLE instFunLikeOrderIso OrderIso.symm	—	—

(root)

Definitions

Name	Category	Theorems
Preord 📖	CompData	36 math math: Preord.ofHom_id, alexDiscEquivPreord_inverse_obj_carrier, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe, Preord.coe_id, Preord.ext_iff, Preord.inv_hom_apply, Preord.hom_inv_apply, alexDiscEquivPreord_inverse_obj_str, Preord.ofHom_apply, Preord.dualEquiv_inverse, alexDiscEquivPreord_inverse_map, instFaithfulPreordCatPreordToCat, Preord.id_apply, Preord.hom_id, Preord.dualEquiv_functor, Preord.forget_map, instFullPreordCatPreordToCat, Preord.hom_comp, Preord.Iso.mk_hom, Preord.dual_map, alexDiscEquivPreord_unitIso, Preord.coe_comp, topToPreord_map, preordToCat_obj, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe', preordToCat_map, topToPreord_obj_coe, SimplexCategory.toCat_obj, Preord.ofHom_comp, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_hom_app_hom_coe, Preord.Iso.mk_inv, alexDiscEquivPreord_counitIso, Preord.comp_apply, SimplexCategory.toCat_map, partOrd_dual_comp_forget_to_preord, alexDiscEquivPreord_functor
preordToCat 📖	CompOp	4 math math: instFaithfulPreordCatPreordToCat, instFullPreordCatPreordToCat, preordToCat_obj, preordToCat_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFaithfulPreordCatPreordToCat 📖	mathematical	—	CategoryTheory.Functor.Faithful Preord Preord.instCategory CategoryTheory.Cat CategoryTheory.Cat.category preordToCat	—	Preord.hom_ext OrderHom.ext CategoryTheory.Functor.congr_obj
instFullPreordCatPreordToCat 📖	mathematical	—	CategoryTheory.Functor.Full Preord Preord.instCategory CategoryTheory.Cat CategoryTheory.Cat.category preordToCat	—	CategoryTheory.Functor.monotone
preordToCat_map 📖	mathematical	—	CategoryTheory.Functor.map Preord Preord.instCategory CategoryTheory.Cat CategoryTheory.Cat.category preordToCat CategoryTheory.Functor.toCatHom Preord.carrier Preorder.smallCategory Preord.str Monotone.functor DFunLike.coe OrderHom OrderHom.instFunLike Preord.Hom.hom	—	—
preordToCat_obj 📖	mathematical	—	CategoryTheory.Functor.obj Preord Preord.instCategory CategoryTheory.Cat CategoryTheory.Cat.category preordToCat CategoryTheory.Cat.of Preord.carrier Preorder.smallCategory Preord.str	—	—

---

← Back to Index