Mathlib v3 is deprecated. Go to Mathlib v4

Theorem set.exists_max_image

Modification history

2022-06-02 17:31
src/data/set/finite.lean
refactor(data/set/finite): protect `set.finite` (#14344) …
Modified set.exists_max_imageView on Github →
2020-04-13 17:33
src/data/set/finite.lean
feat(data/finset): finset lemmas from combinatorics (#2149) …
Added set.exists_max_imageView on Github →