Commit 2023-01-19 14:33 11de62e0

View on Github →

feat: port Data.Finset.Sort (#1675)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finset/Sort.lean

added theorem Finset.coe_orderIsoOfFin_apply

added theorem Finset.length_sort

added theorem Finset.max'_eq_sorted_last

added theorem Finset.mem_sort

added theorem Finset.min'_eq_sorted_zero

added def Finset.orderEmbOfCardLe

added theorem Finset.orderEmbOfCardLe_mem

added def Finset.orderEmbOfFin

added theorem Finset.orderEmbOfFin_apply

added theorem Finset.orderEmbOfFin_eq_orderEmbOfFin_iff

added theorem Finset.orderEmbOfFin_last

added theorem Finset.orderEmbOfFin_mem

added theorem Finset.orderEmbOfFin_singleton

added theorem Finset.orderEmbOfFin_unique'

added theorem Finset.orderEmbOfFin_unique

added theorem Finset.orderEmbOfFin_zero

added def Finset.orderIsoOfFin

added theorem Finset.orderIsoOfFin_symm_apply

added theorem Finset.range_orderEmbOfFin

added def Finset.sort

added theorem Finset.sort_empty

added theorem Finset.sort_eq

added theorem Finset.sort_nodup

added theorem Finset.sort_perm_toList

added theorem Finset.sort_singleton

added theorem Finset.sort_sorted

added theorem Finset.sort_sorted_lt

added theorem Finset.sort_toFinset

added theorem Finset.sorted_last_eq_max'

added theorem Finset.sorted_last_eq_max'_aux

added theorem Finset.sorted_zero_eq_min'

added theorem Finset.sorted_zero_eq_min'_aux