Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes