mathlib
8e0d111f - feat(data/finset/lattice,data/finset/sort): singleton lemmas (#3668)

Commit
5 years ago
feat(data/finset/lattice,data/finset/sort): singleton lemmas (#3668) Add lemmas about `min'`, `max'` and `mono_of_fin` for a singleton `finset`.
Author
Parents
Loading