Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-03 10:04 8e0d111f

View on Github →

feat(data/finset/lattice,data/finset/sort): singleton lemmas (#3668) Add lemmas about min', max' and mono_of_fin for a singleton finset.

Estimated changes

Modified src/data/finset/lattice.lean

added theorem finset.max'_singleton

added theorem finset.min'_singleton

Modified src/data/finset/sort.lean

added theorem finset.mono_of_fin_singleton