mathlib3
b19c491a - chore(order/lattice): rename le_sup_left_of_le (#7856)

Commit

4 years ago

chore(order/lattice): rename le_sup_left_of_le (#7856) rename `le_sup_left_of_le` to `le_sup_of_le_left`, and variants

Author

YaelDillies

Parents