PartOrd

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

Statistics

Metric	Count
Definitions PartOrd, hom, hom, hom', mk, carrier, dual, dualEquiv, hasForgetToPreord, instCategory, instCoeSortType, instConcreteCategoryOrderHomCarrier, ofHom, str, preordToPartOrd, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd, preordToPartOrdForgetAdjunction	17
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, partOrd_dual_comp_forget_to_preord, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_hom_app_hom_coe, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe'	30
Total	47

PartOrd

Definitions

Name	Category	Theorems
carrier 📖	CompOp	70 math math: preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe, SemilatInfCat_dual_comp_forget_to_partOrd, bddOrd_dual_comp_forget_to_bipointed, BddOrd.coe_id, coe_of, BddOrd.hom_id, FinPartOrd.dualEquiv_unitIso, BddOrd.ext_iff, BddLat.forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd, coe_id, BddOrd.Iso.mk_hom, dual_map, BddOrd.dual_map, FinPartOrd.hom_hom_comp, FinBoolAlg.forgetToFinPartOrdFaithful, FinPartOrd.ofHom_hom_hom, BddLat.forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd, bddOrd_dual_comp_forget_to_partOrd, FinPartOrd.dualEquiv_counitIso, coe_comp, SemilatInfCat.coe_forget_to_partOrd, partOrdEmb_dual_comp_forget_to_pardOrd, BddOrd.forget_map, comp_apply, FinPartOrd.dual_map, FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_carrier, inv_hom_apply, ofHom_hom, BddOrd.id_apply, BddOrd.coe_of, bddLat_dual_comp_forget_to_bddOrd, BddLat.forget_lat_partOrd_eq_forget_bddOrd_partOrd, FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_isFintype, BddOrd.Iso.mk_inv, Lat_dual_comp_forget_to_partOrd, BddOrd.hom_comp, FinPartOrd.comp_apply, FinPartOrd.Iso.mk_inv, Iso.mk_hom, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe', FinPartOrd.hom_id, SimplexCategory.toCat_obj, BddOrd.hom_inv_apply, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_hom_app_hom_coe, BddOrd.comp_apply, FinPartOrd_dual_comp_forget_to_partOrd, Iso.mk_inv, BddLat.coe_forget_to_bddOrd, BddOrd.ofHom_apply, FinBoolAlg.hasForgetToFinPartOrd_forget₂_map, hom_inv_apply, BddOrd.ofHom_hom, forget_map, SemilatSupCat_dual_comp_forget_to_partOrd, ofHom_apply, hom_comp, BddOrd.coe_comp, FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_str, FinPartOrd.hom_comp, SimplexCategory.toCat_map, FinPartOrd.Iso.mk_hom, SemilatSupCat.coe_forget_to_partOrd, partOrd_dual_comp_forget_to_preord, BddOrd.inv_hom_apply, ext_iff, FinPartOrd.id_apply, FinPartOrd.ofHom_hom, FinPartOrd.hom_hom_id, hom_id, id_apply
dual 📖	CompOp	13 math math: preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe, SemilatInfCat_dual_comp_forget_to_partOrd, dual_map, dualEquiv_functor, bddOrd_dual_comp_forget_to_partOrd, partOrdEmb_dual_comp_forget_to_pardOrd, Lat_dual_comp_forget_to_partOrd, dualEquiv_inverse, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe', preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_hom_app_hom_coe, FinPartOrd_dual_comp_forget_to_partOrd, SemilatSupCat_dual_comp_forget_to_partOrd, partOrd_dual_comp_forget_to_preord
dualEquiv 📖	CompOp	2 math math: dualEquiv_functor, dualEquiv_inverse
hasForgetToPreord 📖	CompOp	3 math math: SimplexCategory.toCat_obj, SimplexCategory.toCat_map, partOrd_dual_comp_forget_to_preord
instCategory 📖	CompOp	46 math math: preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe, SemilatInfCat_dual_comp_forget_to_partOrd, BddLat.forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd, coe_id, dual_map, dualEquiv_functor, FinPartOrd.hom_ofHom, FinPartOrd.hom_hom_comp, FinPartOrd.ofHom_hom_hom, BddLat.forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd, bddOrd_dual_comp_forget_to_partOrd, coe_comp, SemilatInfCat.coe_forget_to_partOrd, partOrdEmb_dual_comp_forget_to_pardOrd, comp_apply, FinPartOrd.dual_map, inv_hom_apply, ofHom_id, BddLat.forget_lat_partOrd_eq_forget_bddOrd_partOrd, Lat_dual_comp_forget_to_partOrd, dualEquiv_inverse, Iso.mk_hom, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe', FinPartOrd.hom_id, SimplexCategory.toCat_obj, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_hom_app_hom_coe, FinPartOrd_dual_comp_forget_to_partOrd, Iso.mk_inv, FinBoolAlg.hasForgetToFinPartOrd_forget₂_map, hom_inv_apply, forget_map, SemilatSupCat_dual_comp_forget_to_partOrd, ofHom_apply, hom_comp, FinPartOrd.hom_comp, SimplexCategory.toCat_map, SemilatSupCat.coe_forget_to_partOrd, partOrd_dual_comp_forget_to_preord, ofHom_comp, ext_iff, FinPartOrd.ofHom_hom, FinPartOrd.hom_hom_id, hom_id, id_apply, FinPartOrd.hom_hom_ofHom, FinPartOrd.hom_ext_iff
instCoeSortType 📖	CompOp	—
instConcreteCategoryOrderHomCarrier 📖	CompOp	23 math math: SemilatInfCat_dual_comp_forget_to_partOrd, BddLat.forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd, coe_id, BddLat.forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd, bddOrd_dual_comp_forget_to_partOrd, coe_comp, SemilatInfCat.coe_forget_to_partOrd, partOrdEmb_dual_comp_forget_to_pardOrd, comp_apply, inv_hom_apply, BddLat.forget_lat_partOrd_eq_forget_bddOrd_partOrd, Lat_dual_comp_forget_to_partOrd, SimplexCategory.toCat_obj, FinPartOrd_dual_comp_forget_to_partOrd, hom_inv_apply, forget_map, SemilatSupCat_dual_comp_forget_to_partOrd, ofHom_apply, SimplexCategory.toCat_map, SemilatSupCat.coe_forget_to_partOrd, partOrd_dual_comp_forget_to_preord, ext_iff, id_apply
ofHom 📖	CompOp	9 math math: dual_map, hom_ofHom, ofHom_hom, ofHom_id, Iso.mk_hom, Iso.mk_inv, FinBoolAlg.hasForgetToFinPartOrd_forget₂_map, ofHom_apply, ofHom_comp
str 📖	CompOp	58 math math: preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe, SemilatInfCat_dual_comp_forget_to_partOrd, bddOrd_dual_comp_forget_to_bipointed, BddOrd.coe_id, BddOrd.hom_id, BddOrd.ext_iff, BddLat.forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd, coe_id, BddOrd.Iso.mk_hom, dual_map, BddOrd.dual_map, FinPartOrd.hom_hom_comp, BddLat.forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd, bddOrd_dual_comp_forget_to_partOrd, coe_comp, SemilatInfCat.coe_forget_to_partOrd, partOrdEmb_dual_comp_forget_to_pardOrd, BddOrd.forget_map, comp_apply, FinPartOrd.dual_map, inv_hom_apply, ofHom_hom, BddOrd.id_apply, bddLat_dual_comp_forget_to_bddOrd, BddLat.forget_lat_partOrd_eq_forget_bddOrd_partOrd, BddOrd.Iso.mk_inv, Lat_dual_comp_forget_to_partOrd, BddOrd.hom_comp, FinPartOrd.Iso.mk_inv, Iso.mk_hom, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe', FinPartOrd.hom_id, SimplexCategory.toCat_obj, BddOrd.hom_inv_apply, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_hom_app_hom_coe, BddOrd.comp_apply, FinPartOrd_dual_comp_forget_to_partOrd, Iso.mk_inv, BddLat.coe_forget_to_bddOrd, BddOrd.ofHom_apply, hom_inv_apply, BddOrd.ofHom_hom, forget_map, SemilatSupCat_dual_comp_forget_to_partOrd, ofHom_apply, hom_comp, BddOrd.coe_comp, FinBoolAlg.hasForgetToFinPartOrd_forget₂_obj_str, FinPartOrd.hom_comp, SimplexCategory.toCat_map, FinPartOrd.Iso.mk_hom, SemilatSupCat.coe_forget_to_partOrd, partOrd_dual_comp_forget_to_preord, BddOrd.inv_hom_apply, ext_iff, FinPartOrd.hom_hom_id, hom_id, id_apply

Theorems

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

PartOrd.Hom

Definitions

Name	Category	Theorems
hom 📖	CompOp	19 math math: preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe, PartOrd.dual_map, PartOrd.hom_ofHom, FinPartOrd.hom_ofHom, FinPartOrd.hom_hom_comp, FinPartOrd.ofHom_hom_hom, PartOrd.hom_ext_iff, FinPartOrd.dual_map, PartOrd.ofHom_hom, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe', FinPartOrd.hom_id, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_hom_app_hom_coe, PartOrd.hom_comp, FinPartOrd.hom_comp, FinPartOrd.ofHom_hom, FinPartOrd.hom_hom_id, PartOrd.hom_id, FinPartOrd.hom_hom_ofHom, FinPartOrd.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

PartOrd.Hom.Simps

Definitions

Name	Category	Theorems
hom 📖	CompOp	—

PartOrd.Iso

Definitions

Name	Category	Theorems
mk 📖	CompOp	—

Theorems

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

(root)

Definitions

Name	Category	Theorems
PartOrd 📖	CompData	46 math math: preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe, SemilatInfCat_dual_comp_forget_to_partOrd, BddLat.forget_semilatSup_partOrd_eq_forget_bddOrd_partOrd, PartOrd.coe_id, PartOrd.dual_map, PartOrd.dualEquiv_functor, FinPartOrd.hom_ofHom, FinPartOrd.hom_hom_comp, FinPartOrd.ofHom_hom_hom, BddLat.forget_semilatInf_partOrd_eq_forget_bddOrd_partOrd, bddOrd_dual_comp_forget_to_partOrd, PartOrd.coe_comp, SemilatInfCat.coe_forget_to_partOrd, partOrdEmb_dual_comp_forget_to_pardOrd, PartOrd.comp_apply, FinPartOrd.dual_map, PartOrd.inv_hom_apply, PartOrd.ofHom_id, BddLat.forget_lat_partOrd_eq_forget_bddOrd_partOrd, Lat_dual_comp_forget_to_partOrd, PartOrd.dualEquiv_inverse, PartOrd.Iso.mk_hom, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe', FinPartOrd.hom_id, SimplexCategory.toCat_obj, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_hom_app_hom_coe, FinPartOrd_dual_comp_forget_to_partOrd, PartOrd.Iso.mk_inv, FinBoolAlg.hasForgetToFinPartOrd_forget₂_map, PartOrd.hom_inv_apply, PartOrd.forget_map, SemilatSupCat_dual_comp_forget_to_partOrd, PartOrd.ofHom_apply, PartOrd.hom_comp, FinPartOrd.hom_comp, SimplexCategory.toCat_map, SemilatSupCat.coe_forget_to_partOrd, partOrd_dual_comp_forget_to_preord, PartOrd.ofHom_comp, PartOrd.ext_iff, FinPartOrd.ofHom_hom, FinPartOrd.hom_hom_id, PartOrd.hom_id, PartOrd.id_apply, FinPartOrd.hom_hom_ofHom, FinPartOrd.hom_ext_iff
preordToPartOrd 📖	CompOp	3 math math: preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe', preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_hom_app_hom_coe
preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd 📖	CompOp	3 math math: preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe, preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe', preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_hom_app_hom_coe
preordToPartOrdForgetAdjunction 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
partOrd_dual_comp_forget_to_preord 📖	mathematical	—	CategoryTheory.Functor.comp PartOrd PartOrd.instCategory Preord Preord.instCategory PartOrd.dual CategoryTheory.forget₂ OrderHom PartOrd.carrier PartialOrder.toPreorder PartOrd.str OrderHom.instFunLike PartOrd.instConcreteCategoryOrderHomCarrier Preord.carrier Preord.str Preord.instConcreteCategoryOrderHomCarrier PartOrd.hasForgetToPreord Preord.dual	—	—
preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_hom_app_hom_coe 📖	mathematical	—	DFunLike.coe OrderHom PartOrd.carrier CategoryTheory.Functor.obj Preord Preord.instCategory PartOrd PartOrd.instCategory CategoryTheory.Functor.comp preordToPartOrd PartOrd.dual Preord.dual PartialOrder.toPreorder PartOrd.str OrderHom.instFunLike PartOrd.Hom.hom CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd OrderIso Preorder.toLE instFunLikeOrderIso OrderIso.dualAntisymmetrization Preord.carrier Preord.str	—	—
preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe 📖	mathematical	—	DFunLike.coe OrderHom PartOrd.carrier CategoryTheory.Functor.obj Preord Preord.instCategory PartOrd PartOrd.instCategory CategoryTheory.Functor.comp Preord.dual preordToPartOrd PartOrd.dual PartialOrder.toPreorder PartOrd.str OrderHom.instFunLike PartOrd.Hom.hom CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd OrderIso Preorder.toLE instFunLikeOrderIso OrderIso.symm OrderIso.dualAntisymmetrization Preord.carrier Preord.str	—	—
preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd_inv_app_hom_coe' 📖	mathematical	—	DFunLike.coe OrderHom PartOrd.carrier CategoryTheory.Functor.obj Preord Preord.instCategory PartOrd PartOrd.instCategory preordToPartOrd Preord.dual PartOrd.dual PartialOrder.toPreorder PartOrd.str OrderHom.instFunLike PartOrd.Hom.hom CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category preordToPartOrdCompToDualIsoToDualCompPreordToPartOrd OrderIso Antisymmetrization OrderDual Preord.carrier OrderDual.instLE Preorder.toLE Preord.str instIsPreorderLe OrderDual.instPreorder instPartialOrderAntisymmetrization instFunLikeOrderIso OrderIso.symm OrderIso.dualAntisymmetrization	—	—

---

← Back to Index