mathlib
c058607c - chore(order): generalize `min_top_left` (#10486)

Commit

4 years ago

chore(order): generalize `min_top_left` (#10486) As well as its relative `min_top_right`. Also provide `max_bot_(left|right)`.

Author

pechersky

Parents