mathlib
d425e693 - chore(order/complete_lattice): golf a proof (#10607)

Commit

4 years ago

chore(order/complete_lattice): golf a proof (#10607) Also reformulate `le_Sup_iff` in terms of `upper_bounds`.

Author

urkud

Committer

jcommelin

Parents