Tuple.antitone_pair_of_not_sorted
theorem Tuple.antitone_pair_of_not_sorted :
∀ {n : ℕ} {α : Type u_1} [inst : LinearOrder α] {f : Fin n → α},
f ≠ f ∘ ⇑(Tuple.sort f) → ∃ i j, i < j ∧ f j < f i
This theorem states that, for any function `f` from the set of finite ordinal numbers `Fin n` to any linearly ordered type `α`, if `f` is not equivalent to `f` after sorting according to the order of outputs of `f`, then there exists a pair of indices `(i, j)` such that `i` is less than `j` and `f j` is strictly less than `f i`. In other words, if the function does not maintain the same values after being sorted, then there must be at least one pair of strictly decreasing entries in the function.
More concisely: If `f` is a function from finite ordinals to a linearly ordered type such that `f` is not order-preserving, then there exist distinct indices `i` and `j` with `i < j` and `f(i) < f(j)`.
|
Tuple.eq_sort_iff'
theorem Tuple.eq_sort_iff' :
∀ {n : ℕ} {α : Type u_1} [inst : LinearOrder α] {f : Fin n → α} {σ : Equiv.Perm (Fin n)},
σ = Tuple.sort f ↔ StrictMono ⇑(σ.trans (Tuple.graphEquiv₁ f))
The theorem `Tuple.eq_sort_iff'` states that for any natural number `n`, any type `α` with a linear order, any function `f` from the finite set of the first `n` natural numbers to `α`, and any permutation `σ` on the finite set of the first `n` natural numbers, `σ` is equal to the permutation that sorts the set according to the order of the outputs of `f` if and only if the map `i ↦ (f (σ i), σ i)` is strictly monotone with respect to the lexicographic ordering on the target. Here, a function is said to be strictly monotone if `a < b` implies `f(a) < f(b)`. A permutation is a bijection, or a one-to-one correspondence, from a set to itself.
More concisely: A permutation σ on the first n natural numbers sorts the set according to the order of the outputs of a function f from the finite set of the first n natural numbers to type α if and only if the function i ↦ (f (σ i), σ i) is strictly monotone with respect to the lexicographic ordering on α × ℕ.
|
Tuple.antitone_pair_of_not_sorted'
theorem Tuple.antitone_pair_of_not_sorted' :
∀ {n : ℕ} {α : Type u_1} [inst : LinearOrder α] {f : Fin n → α} {σ : Equiv.Perm (Fin n)},
f ∘ ⇑σ ≠ f ∘ ⇑(Tuple.sort f) → ∃ i j, i < j ∧ (f ∘ ⇑σ) j < (f ∘ ⇑σ) i
This theorem states that for any natural number `n`, type `α` with a linear order, function `f` from `Fin n` to `α`, and permutation `σ` of `Fin n`, if the permutation `f ∘ σ` does not result in the same output as `f ∘ sort f` (where `sort` is a permutation that orders `Fin n` according to the order of the outputs of `f`), then there exists a pair of indices `i` and `j` such that `i` is less than `j` and the `j`-th entry of `f ∘ σ` is less than the `i`-th entry of `f ∘ σ`, indicating a strictly decreasing pair of entries under the permutation `σ`.
More concisely: If `f` is a function from `Fin n` to a linearly ordered type `α`, and `σ` is a permutation of `Fin n` such that `f ∘ σ` is not order-preserving with respect to `f ∘ sort`, then there exist indices `i < j` such that the `i`-th element of `f ∘ σ` is strictly less than the `j`-th element of `f ∘ σ`.
|
Tuple.eq_sort_iff
theorem Tuple.eq_sort_iff :
∀ {n : ℕ} {α : Type u_1} [inst : LinearOrder α] {f : Fin n → α} {σ : Equiv.Perm (Fin n)},
σ = Tuple.sort f ↔ Monotone (f ∘ ⇑σ) ∧ ∀ (i j : Fin n), i < j → f (σ i) = f (σ j) → σ i < σ j
The theorem `Tuple.eq_sort_iff` states that for any natural number `n`, type `α` with a linear order, and function `f` from `Fin n` to `α`, a permutation `σ` is equal to the permutation that sorts `Fin n` according to the order of the outputs of `f` if and only if two conditions are met. First, the function `f` composed with the application of `σ` is monotone, i.e., for all `a` and `b` in the domain, if `a` is less than or equal to `b`, then `f` of `a` is less than or equal to `f` of `b`. Second, for all `i` and `j` in `Fin n`, if `i` is less than `j` and `f` of `σ` applied to `i` equals `f` of `σ` applied to `j`, then `σ` applied to `i` is less than `σ` applied to `j`. This means that the permutation that sorts `Fin n` according to the order of the outputs of `f` is the lexicographically smallest permutation `σ` such that `f` composed with the application of `σ` is monotone.
More concisely: A permutation sorts the outputs of a monotone function `f` from `Fin n` to a linearly ordered type `α` if and only if `f` composed with the application of the permutation is monotone and the permutation reorders the inputs according to the order of the outputs.
|
Tuple.unique_monotone
theorem Tuple.unique_monotone :
∀ {n : ℕ} {α : Type u_1} [inst : PartialOrder α] {f : Fin n → α} {σ τ : Equiv.Perm (Fin n)},
Monotone (f ∘ ⇑σ) → Monotone (f ∘ ⇑τ) → f ∘ ⇑σ = f ∘ ⇑τ
This theorem states that if you have a tuple `f` of a certain size `n` and two permutations `σ` and `τ` of the indices of the tuple, and if applying each of these permutations to the tuple always produces a tuple with the same or increasing order, then the two permutations are actually the same. In other words, if both permutations `σ` and `τ` are such that they keep the tuple `f` monotone (i.e., 'a ≤ b' implies 'f a ≤ f b'), then the two permutations must be equal. This holds for any tuple of a type `α` that has a partial order defined on it.
More concisely: If `σ` and `τ` are permutations of indices preserving the monotonicity of a tuple `f` of type `α` with a defined partial order, then `σ` and `τ` are equal.
|
Tuple.sort_eq_refl_iff_monotone
theorem Tuple.sort_eq_refl_iff_monotone :
∀ {n : ℕ} {α : Type u_1} [inst : LinearOrder α] {f : Fin n → α}, Tuple.sort f = Equiv.refl (Fin n) ↔ Monotone f
The theorem `Tuple.sort_eq_refl_iff_monotone` states that for any function `f` from a finite set of natural numbers `Fin n` to a type `α` with a linear order, the permutation that sorts `f` is identical to the identity permutation on `Fin n` if and only if the function `f` is monotone. In other words, if and only if for any two elements `a` and `b` in `Fin n`, `a ≤ b` implies `f(a) ≤ f(b)`.
More concisely: The permutation that sorts a function from a finite set of natural numbers to a type with a linear order is equal to the identity if and only if the function is monotone.
|
Tuple.comp_perm_comp_sort_eq_comp_sort
theorem Tuple.comp_perm_comp_sort_eq_comp_sort :
∀ {n : ℕ} {α : Type u_1} [inst : LinearOrder α] {f : Fin n → α} {σ : Equiv.Perm (Fin n)},
(f ∘ ⇑σ) ∘ ⇑(Tuple.sort (f ∘ ⇑σ)) = f ∘ ⇑(Tuple.sort f)
This theorem states that for any natural number `n`, any type `α` that has a linear order, any function `f` from `Fin n` to `α`, and any permutation `σ` of `Fin n`, the sorted version of the tuple `f` after being permuted by `σ` is the same as the sorted version of the original tuple `f`. In other words, sorting doesn't change even if `f` is permuted before sorting.
More concisely: For any natural number `n`, any linear order `α`, any function `f : Fin n → α`, and any permutation `σ : Fin n → Fin n`, the sorted lists of `[f (σ i) | i ∈ Fin n]` and `[f i | i ∈ Fin n]` are equal.
|
Tuple.comp_sort_eq_comp_iff_monotone
theorem Tuple.comp_sort_eq_comp_iff_monotone :
∀ {n : ℕ} {α : Type u_1} [inst : LinearOrder α] {f : Fin n → α} {σ : Equiv.Perm (Fin n)},
f ∘ ⇑σ = f ∘ ⇑(Tuple.sort f) ↔ Monotone (f ∘ ⇑σ)
The theorem `Tuple.comp_sort_eq_comp_iff_monotone` states that for any natural number `n`, any type `α` with a linear order, any function `f` from `Fin n` to `α`, and any permutation `σ` of `Fin n`, the function `f` composed with the application of `σ` is equal to `f` composed with the application of the sort of `f` if and only if the function `f` composed with the application of `σ` is monotone. In other words, a permutation of a tuple `f` is equivalent to `f` sorted if and only if it is a monotone function.
More concisely: For any function `f` from a finite indexed set to a linearly ordered type, a permutation `σ` of the indices makes `f ∘ σ` equal to `f ∘ sort` if and only if `f ∘ σ` is a monotone function.
|
Tuple.lt_card_le_iff_apply_le_of_monotone
theorem Tuple.lt_card_le_iff_apply_le_of_monotone :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : DecidableRel LE.le] {m : ℕ} (f : Fin m → α) (a : α),
Monotone f → ∀ (j : Fin m), ↑j < Fintype.card { i // f i ≤ a } ↔ f j ≤ a
This theorem states that given a partially ordered type `α` and a natural number `m`, for any `m`-tuple of elements of `α` that is sorted in non-decreasing order (i.e., `f₀ ≤ f₁ ≤ f₂ ≤ ⋯`), and any element `a` of type `α`, if the function `f` that maps indices to the elements of the tuple is monotone (meaning that the elements maintain their order when mapped), then for any index `j` in the `m`-tuple, the condition that `j` is less than the number of elements in the tuple that are less than or equal to `a` is equivalent to the condition that the element at index `j` in the tuple is less than or equal to `a`. This theorem assumes that the less-equal relation `LE.le` is decidable for the type `α`.
More concisely: Given a partially ordered type `α` with decidable `LE.le` relation, for any monotone function `f : ℕ → α` mapping indices to an `m`-tuple `(a₀ ≤ a₁ ≤ ⋯ ≤ aᵢ)` of elements in `α`, and any `a : α`, the index `j` is less than the number of `a`'s predecessors in `(a₀, a₁, ..., aᵢ)` if and only if `aᵢ ≤ a`.
|