Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-19 18:52 344a41e8

View on Github →

feat(data/finset): monotone bijection from fin k (#2163)

feat(data/finset): increasing bijection between fin k and an ordered finset
fix build
fix linter
make argument explicit
add equiv for fintype

Estimated changes

Modified src/data/equiv/basic.lean

added theorem dite_comp_equiv_update

Modified src/data/finset.lean

added theorem finset.bij_on_mono_of_fin

added def finset.mono_of_fin

modified theorem finset.sort_sorted_lt

added theorem finset.sorted_last_eq_max'

added theorem finset.sorted_zero_eq_min'

Modified src/data/fintype.lean

added theorem finset.card_fin

added theorem fintype.card_finset

Modified src/data/list/sort.lean

added theorem list.nth_le_of_sorted_of_le

Modified src/group_theory/sylow.lean