Commit 2021-02-11 06:02 330129d4
View on Github →feat(data/finset/lattice): inf
and sup
on complete_linear_orders produce an element of the set (#6103)
feat(data/finset/lattice): inf
and sup
on complete_linear_orders produce an element of the set (#6103)