lattice): Remove `finset.sup_finset_image` (#18893)

Commit

2 years ago

chore(data/finset/lattice): Remove `finset.sup_finset_image` (#18893) in favor of the identical `finset.sup_image` (up to argument order) in the same file.

Author

YaelDillies

Parents

c7bce281

mathlib c813ed7d - chore(data/finset/lattice): Remove `finset.sup_finset_image` (#18893)

mathlib
c813ed7d - chore(data/finset/lattice): Remove `finset.sup_finset_image` (#18893)