Commit 2025-10-29 09:29 fb07d799

View on Github →

feat(Order/Category): partial orders with order embeddings as morphisms (#30693) This category will be relevant in the study of accessible categories. I am making Johan Commelin a co-author as the new file PartOrdEmb.lean is essentially a copy-paste of PartOrd.Lean.

Estimated changes

added structure PartOrdEmb.Hom
added theorem PartOrdEmb.coe_comp
added theorem PartOrdEmb.coe_id
added theorem PartOrdEmb.coe_of
added theorem PartOrdEmb.comp_apply
added def PartOrdEmb.dual
added theorem PartOrdEmb.ext
added theorem PartOrdEmb.forget_map
added theorem PartOrdEmb.hom_comp
added theorem PartOrdEmb.hom_ext
added theorem PartOrdEmb.hom_id
added theorem PartOrdEmb.hom_ofHom
added theorem PartOrdEmb.id_apply
added theorem PartOrdEmb.ofHom_apply
added theorem PartOrdEmb.ofHom_comp
added theorem PartOrdEmb.ofHom_hom
added theorem PartOrdEmb.ofHom_id
added structure PartOrdEmb