Commit 2023-01-24 10:15 977263ad

View on Github →

feat: port Data.Fin.Tuple.Sort (#1811)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Fin/Tuple/Sort.lean

added theorem Tuple.antitone_pair_of_not_sorted'

added theorem Tuple.antitone_pair_of_not_sorted

added theorem Tuple.comp_perm_comp_sort_eq_comp_sort

added theorem Tuple.comp_sort_eq_comp_iff_monotone

added theorem Tuple.eq_sort_iff'

added theorem Tuple.eq_sort_iff

added theorem Tuple.graph.card

added def Tuple.graph.proj

added def Tuple.graph

added def Tuple.graphEquiv₁

added def Tuple.graphEquiv₂

added theorem Tuple.graphEquiv₂_apply

added theorem Tuple.monotone_proj

added theorem Tuple.monotone_sort

added theorem Tuple.proj_equiv₁'

added theorem Tuple.self_comp_sort

added def Tuple.sort

added theorem Tuple.sort_eq_refl_iff_monotone

added theorem Tuple.unique_monotone