mathlib3
6f2cbde0 - chore(order/lattice): tidy up pi instances (#9305)

Commit
4 years ago
chore(order/lattice): tidy up pi instances (#9305) These were previously defined in the wrong file, and the lemmas were missing the `pi` prefix that is present on `pi.add_apply` etc. This also removes the instance names as they are autogenerated correctly. Finally, this adds new `top_def`, `bot_def`, `sup_def`, and `inf_def` lemmas, which are useful for when wanting to rewrite under the lambda. We already have `zero_def`, `add_def`, etc.
Author
Parents
Loading