Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-06 05:07 7b3c653b

View on Github →

chore(data/finset/lattice): remove unneeded assumptions (#4020)

Estimated changes

Modified src/combinatorics/composition.lean

Modified src/data/finset/lattice.lean

modified theorem finset.le_max'

modified theorem finset.max'_singleton

modified theorem finset.min'_le

modified theorem finset.min'_lt_max'

modified theorem finset.min'_lt_max'_of_card

modified theorem finset.min'_singleton

Modified src/data/finset/sort.lean

added theorem finset.max'_eq_sorted_last

added theorem finset.min'_eq_sorted_zero

modified theorem finset.mono_of_fin_last

modified theorem finset.mono_of_fin_zero

modified theorem finset.sorted_last_eq_max'

added theorem finset.sorted_last_eq_max'_aux

modified theorem finset.sorted_zero_eq_min'

added theorem finset.sorted_zero_eq_min'_aux

Modified src/order/filter/at_top_bot.lean