mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

`partial_order.lift` vs `function.injective.partial_order`

Open eric-wieser opened this issue 3 years ago • 1 comments

Should we rename partial_order.lift to function.injective.partial_order? Or conversely, should the definitions in this PR be called lattice.lift etc? It might be worth polling on Zulip.

Originally posted by @eric-wieser in https://github.com/leanprover-community/mathlib/issues/10615#issuecomment-986035004

As of #10615, we currently have:

  • preorder.lift, partial_order.lift, linear_order.lift
  • function.injective.semilattice_sup, function.injective.lattice_sup, function.injective.lattice (and all the algebra defs named in this way)

We should try to unify these naming conventions. This is made somewhat tricky by the fact that preorder.lift doesn't take a function.injective argument.

eric-wieser avatar Dec 10 '21 11:12 eric-wieser