mathlib

47b1ddf2 - feat(data/setoid/partition): Relate `setoid.is_partition` and `finpartition` (#12459)

feat(data/setoid/partition): Relate `setoid.is_partition` and `finpartition` (#12459) Add two functions that relate `setoid.is_partition` and `finpartition`: * `setoid.is_partition.partition` * `finpartition.is_partition_parts` Meanwhile add some lemmas related to `finset.sup` and `finset.inf` in data/finset/lattice. Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>