mathlib3
3a0b0d1d - chore(order/lattice): add `exists_lt_of_sup/inf` (#10133)

Commit

4 years ago

chore(order/lattice): add `exists_lt_of_sup/inf` (#10133)

Author

urkud

urkud

Parents

Loading