basic): add `finset.order_top` and `finset.bounded_distrib_lattice` (#3345)

Commit

5 years ago

chore(data/fintype/basic): add `finset.order_top` and `finset.bounded_distrib_lattice` (#3345)

Author

urkud

Parents