Commit 2022-03-31 06:51 290f440a

View on Github →

feat(order/category/Semilattice): The categories of semilattices (#12890) Define SemilatticeSup and SemilatticeInf, the categories of finitary supremum lattices and finitary infimum lattices.

Estimated changes

Modified src/order/category/BoundedLattice.lean

added theorem BoundedLattice.coe_forget_to_BoundedOrder

added theorem BoundedLattice.coe_forget_to_Lattice

added theorem BoundedLattice.coe_forget_to_SemilatticeInf

added theorem BoundedLattice.coe_forget_to_SemilatticeSup

added theorem BoundedLattice.forget_SemilatticeInf_PartialOrder_eq_forget_BoundedOrder_PartialOrder

added theorem BoundedLattice.forget_SemilatticeSup_PartialOrder_eq_forget_BoundedOrder_PartialOrder

added theorem BoundedLattice_dual_comp_forget_to_SemilatticeInf

added theorem BoundedLattice_dual_comp_forget_to_SemilatticeSup

Created src/order/category/Semilattice.lean

added theorem SemilatticeInf.coe_forget_to_PartialOrder

added theorem SemilatticeInf.coe_of

added def SemilatticeInf.dual

added def SemilatticeInf.iso.mk

added def SemilatticeInf.of

added structure SemilatticeInf

added theorem SemilatticeInf_dual_comp_forget_to_PartialOrder

added theorem SemilatticeSup.coe_forget_to_PartialOrder

added theorem SemilatticeSup.coe_of

added def SemilatticeSup.dual

added def SemilatticeSup.iso.mk

added def SemilatticeSup.of

added structure SemilatticeSup

added theorem SemilatticeSup_dual_comp_forget_to_PartialOrder

added def SemilatticeSup_equiv_SemilatticeInf