Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-17 13:50 f7899692

View on Github →

feat(data/finset): add min' / max' for non-empty finset

Estimated changes

added theorem finset.filter_true
added theorem finset.le_max'
added theorem finset.le_min'
added theorem finset.lt_wf
added def finset.max'
added theorem finset.max'_le
added theorem finset.max'_mem
added def finset.min'
added theorem finset.min'_le
added theorem finset.min'_lt_max'
added theorem finset.min'_mem