mathlib3
6d02dac3 - feat(order/lattice, order/lattice_intervals): coe inf/sup lemmas (#15136)

Commit
3 years ago
feat(order/lattice, order/lattice_intervals): coe inf/sup lemmas (#15136) This PR adds simp lemmas for coercions of inf/sup in order instances on intervals. We also change the order of some arguments in instances/lemmas, by removing `variables` commands, so that typeclass arguments precede others. Co-authored-by: Peter Nelson <apnelson@uwaterloo.ca>
Author
Parents
Loading