Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finset.sup_finset_image

Modification history

2023-04-28 14:14
src/data/finset/lattice.lean
chore(data/finset/lattice): Remove `finset.sup_finset_image` (#18893) …
Deleted finset.sup_finset_imageView on Github →
2021-11-23 13:11
src/data/finset/lattice.lean
refactor(*): split `order_{top,bot}` from `lattice` hierarchy (#9891) …
Modified finset.sup_finset_imageView on Github →
2021-03-26 14:24
src/data/finset/lattice.lean
feat(ring_theory/polynomial/symmetric): degrees_esymm (#6718) …
Modified finset.sup_finset_imageView on Github →
2021-01-27 08:41
src/data/finset/lattice.lean
feat(ring_theory/noetherian, linear_algebra/basic): Show that finitely generated submodules are the compact elements in the submodule lattice (#5871) …
Added finset.sup_finset_imageView on Github →