Commit 2025-02-10 08:46 63edd591

View on Github →

refactor(Order/Category): concrete category refactor for basic orders (#21409) This PR implements Hom classes and ConcreteCategory instances for the following categories of orders:

Estimated changes

added structure BddDistLat.Hom
added theorem BddDistLat.coe_comp
added theorem BddDistLat.coe_id
added theorem BddDistLat.comp_apply
added theorem BddDistLat.ext
added theorem BddDistLat.forget_map
added theorem BddDistLat.hom_comp
added theorem BddDistLat.hom_ext
added theorem BddDistLat.hom_id
added theorem BddDistLat.hom_ofHom
added theorem BddDistLat.id_apply
deleted def BddDistLat.of
added theorem BddDistLat.ofHom_apply
added theorem BddDistLat.ofHom_comp
added theorem BddDistLat.ofHom_hom
added theorem BddDistLat.ofHom_id
modified structure BddDistLat
added structure BddLat.Hom
added theorem BddLat.comp_apply
added theorem BddLat.ext
added theorem BddLat.hom_comp
added theorem BddLat.hom_ext
added theorem BddLat.hom_id
added theorem BddLat.id_apply
deleted def BddLat.of
modified structure BddLat
added structure BddOrd.Hom
added theorem BddOrd.coe_comp
added theorem BddOrd.coe_id
modified theorem BddOrd.coe_of
added theorem BddOrd.comp_apply
added theorem BddOrd.ext
added theorem BddOrd.forget_map
added theorem BddOrd.hom_comp
added theorem BddOrd.hom_ext
added theorem BddOrd.hom_id
added theorem BddOrd.hom_inv_apply
added theorem BddOrd.hom_ofHom
added theorem BddOrd.id_apply
added theorem BddOrd.inv_hom_apply
deleted def BddOrd.of
added theorem BddOrd.ofHom_apply
added theorem BddOrd.ofHom_comp
added theorem BddOrd.ofHom_hom
added theorem BddOrd.ofHom_id
modified structure BddOrd
added structure BoolAlg.Hom
added theorem BoolAlg.coe_comp
added theorem BoolAlg.coe_id
modified theorem BoolAlg.coe_of
added theorem BoolAlg.comp_apply
added theorem BoolAlg.ext
added theorem BoolAlg.forget_map
added theorem BoolAlg.hom_comp
added theorem BoolAlg.hom_ext
added theorem BoolAlg.hom_id
added theorem BoolAlg.hom_inv_apply
added theorem BoolAlg.hom_ofHom
added theorem BoolAlg.id_apply
added theorem BoolAlg.inv_hom_apply
deleted def BoolAlg.of
added theorem BoolAlg.ofHom_apply
added theorem BoolAlg.ofHom_comp
added theorem BoolAlg.ofHom_hom
added theorem BoolAlg.ofHom_id
added structure BoolAlg
deleted def BoolAlg
added structure DistLat.Hom
added theorem DistLat.coe_comp
added theorem DistLat.coe_id
modified theorem DistLat.coe_of
added theorem DistLat.comp_apply
added theorem DistLat.ext
added theorem DistLat.forget_map
added theorem DistLat.hom_comp
added theorem DistLat.hom_ext
added theorem DistLat.hom_id
added theorem DistLat.hom_inv_apply
added theorem DistLat.hom_ofHom
added theorem DistLat.id_apply
added theorem DistLat.inv_hom_apply
deleted def DistLat.of
added theorem DistLat.ofHom_apply
added theorem DistLat.ofHom_comp
added theorem DistLat.ofHom_hom
added theorem DistLat.ofHom_id
added structure DistLat
deleted def DistLat
added structure FinBddDistLat.Hom
modified def FinBddDistLat.Iso.mk
added theorem FinBddDistLat.coe_comp
added theorem FinBddDistLat.coe_id
added theorem FinBddDistLat.ext
added theorem FinBddDistLat.hom_comp
added theorem FinBddDistLat.hom_ext
added theorem FinBddDistLat.hom_id
added theorem FinBddDistLat.id_apply
deleted def FinBddDistLat.of'
deleted def FinBddDistLat.of
added theorem FinBddDistLat.ofHom_id
modified structure FinBddDistLat
deleted def FinBoolAlg.of
modified structure FinBoolAlg
deleted theorem FinPartOrd.coe_of
added theorem FinPartOrd.comp_apply
added theorem FinPartOrd.hom_comp
added theorem FinPartOrd.hom_ext
added theorem FinPartOrd.hom_id
added theorem FinPartOrd.hom_ofHom
added theorem FinPartOrd.id_apply
deleted def FinPartOrd.of
added theorem FinPartOrd.ofHom_hom
modified structure FinPartOrd
added structure Frm.Hom
added theorem Frm.coe_comp
added theorem Frm.coe_id
modified theorem Frm.coe_of
added theorem Frm.comp_apply
added theorem Frm.ext
added theorem Frm.forget_map
added theorem Frm.hom_comp
added theorem Frm.hom_ext
added theorem Frm.hom_id
added theorem Frm.hom_inv_apply
added theorem Frm.hom_ofHom
added theorem Frm.id_apply
added theorem Frm.inv_hom_apply
deleted def Frm.of
added theorem Frm.ofHom_apply
added theorem Frm.ofHom_comp
added theorem Frm.ofHom_hom
added theorem Frm.ofHom_id
added structure Frm
deleted def Frm
added structure HeytAlg.Hom
added theorem HeytAlg.coe_comp
added theorem HeytAlg.coe_id
modified theorem HeytAlg.coe_of
added theorem HeytAlg.comp_apply
added theorem HeytAlg.ext
added theorem HeytAlg.forget_map
added theorem HeytAlg.hom_comp
added theorem HeytAlg.hom_ext
added theorem HeytAlg.hom_id
added theorem HeytAlg.hom_inv_apply
added theorem HeytAlg.hom_ofHom
added theorem HeytAlg.id_apply
added theorem HeytAlg.inv_hom_apply
deleted def HeytAlg.of
added theorem HeytAlg.ofHom_apply
added theorem HeytAlg.ofHom_comp
added theorem HeytAlg.ofHom_hom
added theorem HeytAlg.ofHom_id
added structure HeytAlg
deleted def HeytAlg
added structure Lat.Hom
added theorem Lat.coe_comp
added theorem Lat.coe_id
modified theorem Lat.coe_of
added theorem Lat.comp_apply
added theorem Lat.ext
added theorem Lat.forget_map
added theorem Lat.hom_comp
added theorem Lat.hom_ext
added theorem Lat.hom_id
added theorem Lat.hom_inv_apply
added theorem Lat.hom_ofHom
added theorem Lat.id_apply
added theorem Lat.inv_hom_apply
deleted def Lat.of
added theorem Lat.ofHom_apply
added theorem Lat.ofHom_comp
added theorem Lat.ofHom_hom
added theorem Lat.ofHom_id
added structure Lat
deleted def Lat
added structure LinOrd.Hom
added theorem LinOrd.coe_comp
added theorem LinOrd.coe_id
modified theorem LinOrd.coe_of
added theorem LinOrd.comp_apply
added theorem LinOrd.ext
added theorem LinOrd.forget_map
added theorem LinOrd.hom_comp
added theorem LinOrd.hom_ext
added theorem LinOrd.hom_id
added theorem LinOrd.hom_inv_apply
added theorem LinOrd.hom_ofHom
added theorem LinOrd.id_apply
added theorem LinOrd.inv_hom_apply
deleted def LinOrd.of
added theorem LinOrd.ofHom_apply
added theorem LinOrd.ofHom_comp
added theorem LinOrd.ofHom_hom
added theorem LinOrd.ofHom_id
added structure LinOrd
deleted def LinOrd
modified theorem NonemptyFinLinOrd.coe_of
added structure NonemptyFinLinOrd
deleted def NonemptyFinLinOrd
added structure PartOrd.Hom
added theorem PartOrd.coe_comp
added theorem PartOrd.coe_id
modified theorem PartOrd.coe_of
added theorem PartOrd.comp_apply
added theorem PartOrd.ext
added theorem PartOrd.forget_map
added theorem PartOrd.hom_comp
added theorem PartOrd.hom_ext
added theorem PartOrd.hom_id
added theorem PartOrd.hom_inv_apply
added theorem PartOrd.hom_ofHom
added theorem PartOrd.id_apply
added theorem PartOrd.inv_hom_apply
deleted def PartOrd.of
added theorem PartOrd.ofHom_apply
added theorem PartOrd.ofHom_comp
added theorem PartOrd.ofHom_hom
added theorem PartOrd.ofHom_id
added structure PartOrd
deleted def PartOrd
added structure Preord.Hom
added theorem Preord.coe_comp
added theorem Preord.coe_id
modified theorem Preord.coe_of
added theorem Preord.comp_apply
added theorem Preord.ext
added theorem Preord.forget_map
added theorem Preord.hom_comp
added theorem Preord.hom_ext
added theorem Preord.hom_id
added theorem Preord.hom_inv_apply
added theorem Preord.hom_ofHom
added theorem Preord.id_apply
added theorem Preord.inv_hom_apply
deleted def Preord.of
added theorem Preord.ofHom_apply
added theorem Preord.ofHom_comp
added theorem Preord.ofHom_hom
added theorem Preord.ofHom_id
added structure Preord
deleted def Preord
deleted def SemilatInfCat.of
deleted def SemilatSupCat.of