# Commit 2023-08-31 08:51 442a83d7

View on Github →feat(data/finset/lattice): `sup'`

/`inf'`

lemmas (#18989)
Match (most of) the lemmas between `finset.sup`

/`finset.inf`

and `finset.sup'`

/`finset.inf'`

. Also golf two proofs using `eq_of_forall_ge_iff`

to make sure both APIs prove their lemmas in as closely as possible a way. Also define `finset.nontrivial`

to match `set.nontrivial`

.