Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-28 23:45 e8ac6315

View on Github →

chore(order/category): Rename categories (#18657) The Lean 4 naming convention forces us to rename the categories of orders. Instead of blankly appending Cat to the names, we proactively shorten the names. Incidentally, this gets them closer to the way they're referred in the literature.

  • Preorder → Preord (the literature name is Ord, but Lean 4 already takes it)
  • PartialOrder → PartOrd
  • BoundedOrder → BddOrd
  • FinPartialOrder → FinPartOrd
  • SemilatticeSup → SemilatSup
  • SemilatticeInf → SemilatInf
  • Lattice → Lat
  • DistribLattice → DistLat
  • BoundedLattice → BddLat
  • BoundedDistribLattice → BddDistLat
  • LinearOrder → LinOrd
  • CompleteLattice → CompleteLat
  • Frame → Frm (the corresponding class is Order.Frame, but better be safe)

Estimated changes

added theorem BddDistLat.coe_of
added def BddDistLat.dual
added def BddDistLat.of
added structure BddDistLat
added theorem BddLat.coe_of
added def BddLat.dual
added def BddLat.iso.mk
added def BddLat.of
added structure BddLat
added theorem BddOrd.coe_of
added def BddOrd.dual
added def BddOrd.iso.mk
added def BddOrd.of
added structure BddOrd
deleted structure BoundedDistribLattice
deleted theorem BoundedLattice.coe_of
deleted def BoundedLattice.dual
deleted def BoundedLattice.of
deleted structure BoundedLattice
deleted theorem BoundedOrder.coe_of
deleted def BoundedOrder.dual
deleted def BoundedOrder.iso.mk
deleted def BoundedOrder.of
deleted structure BoundedOrder
added theorem CompleteLat.coe_of
added def CompleteLat.dual
added def CompleteLat.of
added def CompleteLat
deleted theorem CompleteLattice.coe_of
deleted def CompleteLattice.of
deleted def CompleteLattice
added theorem DistLat.coe_of
added def DistLat.dual
added def DistLat.iso.mk
added def DistLat.of
added def DistLat
deleted theorem DistribLattice.coe_of
deleted def DistribLattice.dual
deleted def DistribLattice.of
deleted def DistribLattice
added theorem FinPartOrd.coe_of
added def FinPartOrd.dual
added def FinPartOrd.of
added structure FinPartOrd
deleted theorem FinPartialOrder.coe_of
deleted def FinPartialOrder.of
deleted structure FinPartialOrder
deleted theorem Frame.coe_of
deleted def Frame.hom
deleted def Frame.iso.mk
deleted def Frame.of
deleted def Frame
added theorem Frm.coe_of
added def Frm.hom
added def Frm.iso.mk
added def Frm.of
added def Frm
modified def Top_op_to_Frame
added theorem Lat.coe_of
added def Lat.dual
added def Lat.dual_equiv
added def Lat.iso.mk
added def Lat.of
added def Lat
deleted theorem Lattice.coe_of
deleted def Lattice.dual
deleted def Lattice.dual_equiv
deleted def Lattice.iso.mk
deleted def Lattice.of
deleted def Lattice
added theorem LinOrd.coe_of
added def LinOrd.dual
added def LinOrd.iso.mk
added def LinOrd.of
added def LinOrd
deleted theorem LinearOrder.coe_of
deleted def LinearOrder.dual
deleted def LinearOrder.iso.mk
deleted def LinearOrder.of
deleted def LinearOrder
added theorem PartOrd.coe_of
added def PartOrd.dual
added def PartOrd.iso.mk
added def PartOrd.of
added def PartOrd
deleted theorem PartialOrder.coe_of
deleted def PartialOrder.dual
deleted def PartialOrder.iso.mk
deleted def PartialOrder.of
deleted def PartialOrder
added theorem Preord.coe_of
added def Preord.dual
added def Preord.iso.mk
added def Preord.of
added def Preord
added def Preord_to_Cat
deleted theorem Preorder.coe_of
deleted def Preorder.dual
deleted def Preorder.dual_equiv
deleted def Preorder.iso.mk
deleted def Preorder.of
deleted def Preorder
deleted def Preorder_to_Cat
added theorem SemilatInf.coe_of
added def SemilatInf.dual
added def SemilatInf.of
added structure SemilatInf
added theorem SemilatSup.coe_of
added def SemilatSup.dual
added def SemilatSup.of
added structure SemilatSup
deleted theorem SemilatticeInf.coe_of
deleted def SemilatticeInf.dual
deleted def SemilatticeInf.of
deleted structure SemilatticeInf
deleted theorem SemilatticeSup.coe_of
deleted def SemilatticeSup.dual
deleted def SemilatticeSup.of
deleted structure SemilatticeSup
modified def Locale.of
modified def Locale