Theorems · Theorem · combinatorics
Tuple.monotone_sort
∀ {n : ℕ} {α : Type u_1} [inst : LinearOrder α] (f : Fin n → α), Monotone (f ∘ ⇑(Tuple.sort f))- Defined in
- Mathlib.Data.Fin.Tuple.Sort
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 82 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.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- LinearOrderstatement and proof · cited by 8,572
- Monotonestatement and proof · cited by 1,397
- Equiv.Permstatement · cited by 1,375
- Monotone.compproof · cited by 67
- OrderIso.monotoneproof · cited by 23
- Tuple.sortstatement · cited by 19
- Tuple.graphEquiv₂proof · cited by 4
- Tuple.monotone_projproof · cited by 2
- Tuple.self_comp_sortproof · cited by 1
Cited by3
Results whose statement or proof uses this declaration.
- LinearMap.IsSymmetric.eigenvalues_antitoneproof · cited by 3
- Tuple.comp_sort_eq_comp_iff_monotoneproof · cited by 1
- Tuple.comp_perm_comp_sort_eq_comp_sortproof · cited by 0