Documentation

Mathlib.Data.Fin.Tuple.Sort

Sorting tuples by their values #

Given an n-tuple f : Fin n → α where α is ordered, we may want to turn it into a sorted n-tuple. This file provides an API for doing so, with the sorted n-tuple given by f ∘ Tuple.sort f.

Main declarations #

def Tuple.graph {n : } {α : Type u_1} [LinearOrder α] (f : Fin nα) :
Finset (Lex (α × Fin n))

graph f produces the finset of pairs (f i, i) equipped with the lexicographic order.

Equations
Instances For
    def Tuple.graph.proj {n : } {α : Type u_1} [LinearOrder α] {f : Fin nα} :
    { x : Lex (α × Fin n) // x Tuple.graph f }α

    Given p : α ×ₗ (Fin n) := (f i, i) with p ∈ graph f, graph.proj p is defined to be f i.

    Equations
    Instances For
      @[simp]
      theorem Tuple.graph.card {n : } {α : Type u_1} [LinearOrder α] (f : Fin nα) :
      (Tuple.graph f).card = n
      def Tuple.graphEquiv₁ {n : } {α : Type u_1} [LinearOrder α] (f : Fin nα) :
      Fin n { x : Lex (α × Fin n) // x Tuple.graph f }

      graphEquiv₁ f is the natural equivalence between Fin n and graph f, mapping i to (f i, i).

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem Tuple.proj_equiv₁' {n : } {α : Type u_1} [LinearOrder α] (f : Fin nα) :
        Tuple.graph.proj (Tuple.graphEquiv₁ f) = f
        def Tuple.graphEquiv₂ {n : } {α : Type u_1} [LinearOrder α] (f : Fin nα) :
        Fin n ≃o { x : Lex (α × Fin n) // x Tuple.graph f }

        graphEquiv₂ f is an equivalence between Fin n and graph f that respects the order.

        Equations
        Instances For
          def Tuple.sort {n : } {α : Type u_1} [LinearOrder α] (f : Fin nα) :

          sort f is the permutation that orders Fin n according to the order of the outputs of f.

          Equations
          Instances For
            theorem Tuple.graphEquiv₂_apply {n : } {α : Type u_1} [LinearOrder α] (f : Fin nα) (i : Fin n) :
            theorem Tuple.self_comp_sort {n : } {α : Type u_1} [LinearOrder α] (f : Fin nα) :
            f (Tuple.sort f) = Tuple.graph.proj (Tuple.graphEquiv₂ f)
            theorem Tuple.monotone_proj {n : } {α : Type u_1} [LinearOrder α] (f : Fin nα) :
            Monotone Tuple.graph.proj
            theorem Tuple.monotone_sort {n : } {α : Type u_1} [LinearOrder α] (f : Fin nα) :
            theorem Tuple.lt_card_le_iff_apply_le_of_monotone {α : Type u_1} [PartialOrder α] [DecidableRel LE.le] {m : } (f : Fin mα) (a : α) (h_sorted : Monotone f) (j : Fin m) :
            j < Fintype.card { i : Fin m // f i a } f j a

            If f₀ ≤ f₁ ≤ f₂ ≤ ⋯ is a sorted m-tuple of elements of α, then for any j : Fin m and a : α we have j < #{i | fᵢ ≤ a} iff fⱼ ≤ a.

            theorem Tuple.lt_card_ge_iff_apply_ge_of_antitone {α : Type u_1} [PartialOrder α] [DecidableRel LE.le] {m : } (f : Fin mα) (a : α) (h_sorted : Antitone f) (j : Fin m) :
            j < Fintype.card { i : Fin m // a f i } a f j
            theorem Tuple.unique_monotone {n : } {α : Type u_1} [PartialOrder α] {f : Fin nα} {σ : Equiv.Perm (Fin n)} {τ : Equiv.Perm (Fin n)} (hfσ : Monotone (f σ)) (hfτ : Monotone (f τ)) :
            f σ = f τ

            If two permutations of a tuple f are both monotone, then they are equal.

            theorem Tuple.eq_sort_iff' {n : } {α : Type u_1} [LinearOrder α] {f : Fin nα} {σ : Equiv.Perm (Fin n)} :

            A permutation σ equals sort f if and only if the map i ↦ (f (σ i), σ i) is strictly monotone (w.r.t. the lexicographic ordering on the target).

            theorem Tuple.eq_sort_iff {n : } {α : Type u_1} [LinearOrder α] {f : Fin nα} {σ : Equiv.Perm (Fin n)} :
            σ = Tuple.sort f Monotone (f σ) ∀ (i j : Fin n), i < jf (σ i) = f (σ j)σ i < σ j

            A permutation σ equals sort f if and only if f ∘ σ is monotone and whenever i < j and f (σ i) = f (σ j), then σ i < σ j. This means that sort f is the lexicographically smallest permutation σ such that f ∘ σ is monotone.

            theorem Tuple.sort_eq_refl_iff_monotone {n : } {α : Type u_1} [LinearOrder α] {f : Fin nα} :

            The permutation that sorts f is the identity if and only if f is monotone.

            theorem Tuple.comp_sort_eq_comp_iff_monotone {n : } {α : Type u_1} [LinearOrder α] {f : Fin nα} {σ : Equiv.Perm (Fin n)} :
            f σ = f (Tuple.sort f) Monotone (f σ)

            A permutation of a tuple f is f sorted if and only if it is monotone.

            theorem Tuple.comp_perm_comp_sort_eq_comp_sort {n : } {α : Type u_1} [LinearOrder α] {f : Fin nα} {σ : Equiv.Perm (Fin n)} :
            (f σ) (Tuple.sort (f σ)) = f (Tuple.sort f)

            The sorted versions of a tuple f and of any permutation of f agree.

            theorem Tuple.antitone_pair_of_not_sorted' {n : } {α : Type u_1} [LinearOrder α] {f : Fin nα} {σ : Equiv.Perm (Fin n)} (h : f σ f (Tuple.sort f)) :
            ∃ (i : Fin n) (j : Fin n), i < j (f σ) j < (f σ) i

            If a permutation f ∘ σ of the tuple f is not the same as f ∘ sort f, then f ∘ σ has a pair of strictly decreasing entries.

            theorem Tuple.antitone_pair_of_not_sorted {n : } {α : Type u_1} [LinearOrder α] {f : Fin nα} (h : f f (Tuple.sort f)) :
            ∃ (i : Fin n) (j : Fin n), i < j f j < f i

            If the tuple f is not the same as f ∘ sort f, then f has a pair of strictly decreasing entries.