mathlib

40213d84 - feat(data/finset/lattice): four lemmas about non-membership and max/min (#16192)

feat(data/finset/lattice): four lemmas about non-membership and max/min (#16192) These four lemmas were proved and used by Eric in his decidable version of `finsupp.lex`, replacing my previous undecidable one. They are extracted from #15984 (now closed) and used in #16127 (which replaces the closed PR). Authored-by: Eric Wieser <[wieser.eric@gmail.com](mailto:wieser.eric@gmail.com)> Submitted by me :smile: