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.

  • PreorderPreord (the literature name is Ord, but Lean 4 already takes it)
  • PartialOrderPartOrd
  • BoundedOrderBddOrd
  • FinPartialOrderFinPartOrd
  • SemilatticeSupSemilatSup
  • SemilatticeInfSemilatInf
  • LatticeLat
  • DistribLatticeDistLat
  • BoundedLatticeBddLat
  • BoundedDistribLatticeBddDistLat
  • LinearOrderLinOrd
  • CompleteLatticeCompleteLat
  • FrameFrm (the corresponding class is Order.Frame, but better be safe)

Estimated changes

deleted theorem Frame.coe_of
deleted def Frame.hom
deleted def
deleted def Frame.of
deleted def Frame
added theorem Frm.coe_of
added def Frm.hom
added def
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
added def Lat.of
added def Lat
added theorem Preord.coe_of
added def Preord.dual
added def
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
deleted def Preorder.of
deleted def Preorder
deleted def Preorder_to_Cat