lattice): `inf` and `sup` on complete_linear_orders produce an element of the set (#6103)

Commit

4 years ago

feat(data/finset/lattice): `inf` and `sup` on complete_linear_orders produce an element of the set (#6103)

Author

eric-wieser

Parents