Theorems · Definition · combinatorics
Tuple.sort
{n : ℕ} → {α : Type u_1} → [LinearOrder α] → (Fin n → α) → Equiv.Perm (Fin n)sort f is the permutation that orders Fin n according to the order of the outputs of f.
- Defined in
- Mathlib.Data.Fin.Tuple.Sort
- Cited by
- 19 results in Mathlib
- Foundations
- Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- LinearOrder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- LinearOrderstatement and proof · cited by 8,572
- Equiv.symmproof · cited by 3,681
- Equiv.Permstatement · cited by 1,375
- Equiv.transproof · cited by 337
- RelIso.toEquivproof · cited by 113
- Tuple.graphEquiv₁proof · cited by 5
- Tuple.graphEquiv₂proof · cited by 4
Cited by19
Results whose statement or proof uses this declaration.
- LinearMap.IsSymmetric.eigenvalues_defstatement and proof · cited by 4
- Tuple.monotone_sortstatement · cited by 3
- LinearMap.IsSymmetric.eigenvalues_antitoneproof · cited by 3
- Tuple.eq_sort_iffstatement · cited by 2
- LinearMap.IsSymmetric.hasEigenvector_eigenvectorBasisproof · cited by 2
- Tuple.antitone_pair_of_not_sorted'statement and proof · cited by 2
- Tuple.bubble_sort_induction'statement and proof · cited by 1
- Tuple.comp_sort_eq_comp_iff_monotonestatement and proof · cited by 1
- Tuple.eq_sort_iff'statement and proof · cited by 1
- Tuple.self_comp_sortstatement · cited by 1
- LinearMap.IsSymmetric.card_filter_eigenvalues_eqproof · cited by 1
- Tuple.sort_eq_refl_iff_monotonestatement · cited by 1