Finset.orderEmbOfFin_unique
theorem Finset.orderEmbOfFin_unique :
∀ {α : Type u_1} [inst : LinearOrder α] {s : Finset α} {k : ℕ} (h : s.card = k) {f : Fin k → α},
(∀ (x : Fin k), f x ∈ s) → StrictMono f → f = ⇑(s.orderEmbOfFin h)
The theorem `Finset.orderEmbOfFin_unique` states that for any set `s` of type `α` with a linear order and cardinality `k`, any strictly monotone (strictly increasing) function `f` from the finite set `Fin k` to `s` must be identical to the function `orderEmbOfFin s h` where `h` is the proof that the cardinality of `s` is `k`. This essentially means that any strictly increasing map from a finite set to a set of the same size must be the same as the standard increasing bijection (an order-preserving one-to-one correspondence) between these two sets.
More concisely: For any set `s` of type `α` with a linear order and cardinality `k`, any strictly monotone function from `Fin k` to `s` is equal to the standard order-preserving bijection `orderEmbOfFin s h` for the proof of `s` having cardinality `k`.
|
Finset.range_orderEmbOfFin
theorem Finset.range_orderEmbOfFin :
∀ {α : Type u_1} [inst : LinearOrder α] (s : Finset α) {k : ℕ} (h : s.card = k),
Set.range ⇑(s.orderEmbOfFin h) = ↑s
The theorem `Finset.range_orderEmbOfFin` states that for any given type `α` under a linear order, and any finite set `s` of type `α`, if `k` is the cardinality of `s`, then the range of the function obtained by applying the `Finset.orderEmbOfFin` function to `s` and `k` equals the finite set `s` itself. In other words, every element in the finite set `s` is an output of the function `Finset.orderEmbOfFin s h`, where `h` is a proof that `s` has `k` elements.
More concisely: For any linear order type `α` and finite set `s` of size `k` in `α`, `Finset.orderEmbOfFin s h` equals `s`, where `h` is the proof of `s` having size `k`.
|
Finset.sort_nodup
theorem Finset.sort_nodup :
∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r] [inst_2 : IsAntisymm α r]
[inst_3 : IsTotal α r] (s : Finset α), (Finset.sort r s).Nodup
The theorem `Finset.sort_nodup` states that for any type `α`, any decidable relation `r` on `α` which is transitive, antisymmetric and total, and any finset `s` of type `α`, the list that results from sorting `s` using the relation `r` has no duplicate elements. In other words, for any given set of items and a specific way of ordering those items, if you sort the set according to that order, you will get a list where each item appears at most once.
More concisely: For any type `α`, decidable relation `r` on `α` that is transitive, antisymmetric, and total, and any finset `s` of `α`, the sorted list `s.to_list.sort r` has no duplicate elements.
|
Finset.orderEmbOfFin_last
theorem Finset.orderEmbOfFin_last :
∀ {α : Type u_1} [inst : LinearOrder α] {s : Finset α} {k : ℕ} (h : s.card = k) (hz : 0 < k),
(s.orderEmbOfFin h) ⟨k - 1, ⋯⟩ = s.max' ⋯
The theorem `Finset.orderEmbOfFin_last` states that for any type `α` with a linear order, any finite set `s` of that type, and any natural number `k` such that the cardinality of `s` is `k`, if `k` is greater than zero, then the bijective function `orderEmbOfFin` applied to `k-1` equals the maximum value in the set `s`. Here, `orderEmbOfFin` is a function that creates an order-preserving bijection between `Finset.range k` and `s`.
More concisely: For any type `α` with a linear order, any finite set `s` of cardinality `k > 0` from `α`, the function `orderEmbOfFin (k - 1)` is the maximum element of `s`.
|
Finset.sort_sorted
theorem Finset.sort_sorted :
∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r] [inst_2 : IsAntisymm α r]
[inst_3 : IsTotal α r] (s : Finset α), List.Sorted r (Finset.sort r s)
The theorem `Finset.sort_sorted` states that for any type `α` and any relation `r` on `α` that is a decidable, transitive, antisymmetric and total relation, the list obtained by sorting a finset `s` of `α` using the relation `r` is a sorted list with respect to the relation `r`. In other words, given a set of elements, if we have a rule to decide the order between any two elements and this order is consistent (transitive, antisymmetric, and total), then the list obtained by sorting the set using our rule will indeed be sorted according to our order rule.
More concisely: For any decidable, transitive, antisymmetric, and total relation `r` on a type `α`, sorting a finset of `α` using `r` results in a sorted list with respect to `r`.
|
Finset.orderEmbOfFin_eq_orderEmbOfFin_iff
theorem Finset.orderEmbOfFin_eq_orderEmbOfFin_iff :
∀ {α : Type u_1} [inst : LinearOrder α] {k l : ℕ} {s : Finset α} {i : Fin k} {j : Fin l} {h : s.card = k}
{h' : s.card = l}, (s.orderEmbOfFin h) i = (s.orderEmbOfFin h') j ↔ ↑i = ↑j
The theorem `Finset.orderEmbOfFin_eq_orderEmbOfFin_iff` states that for any type `α` with a linear order, given two natural numbers `k` and `l`, a finite set `s` of type `α`, and two elements `i` from the finite set `Fin k` and `j` from the finite set `Fin l`, if the cardinality of `s` is equal to both `k` and `l`, then the parametrizations `orderEmbOfFin` of `s` as ordered by `k` and `l` respectively, map `i` and `j` to the same value if and only if `i` and `j` are the same element when considered as natural numbers. This statement holds even though `Fin k` and `Fin l` may not be definitionally equal types, although it's necessarily the case that `k = l`.
More concisely: For any type with a linear order and finite sets of different sizes, the parametrized order embeddings map equal elements as natural numbers to the same image if and only if the sets have the same cardinality.
|
Finset.length_sort
theorem Finset.length_sort :
∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r] [inst_2 : IsAntisymm α r]
[inst_3 : IsTotal α r] {s : Finset α}, (Finset.sort r s).length = s.card
The theorem `Finset.length_sort` states that for any type `α`, and any relation `r` on `α` which is decidable, transitive, antisymmetric, and total, the length of the list obtained by sorting a finite set `s` of `α` elements according to `r` is equal to the cardinality of the set `s`. In other words, sorting the elements of the set `s` into a list does not change the number of elements.
More concisely: For any type `α` and decidable, transitive, antisymmetric, and total relation `r` on `α`, the length of the list obtained by sorting a finite set of `α` elements according to `r` equals the cardinality of the set.
|
Finset.orderEmbOfFin_singleton
theorem Finset.orderEmbOfFin_singleton :
∀ {α : Type u_1} [inst : LinearOrder α] (a : α) (i : Fin 1), ({a}.orderEmbOfFin ⋯) i = a
The theorem `Finset.orderEmbOfFin_singleton` states that, for any type `α` that has a linear order, and any element `a` of type `α`, the function `orderEmbOfFin` when applied on a singleton set containing only `a`, will map every element of a finite set of size 1 (`Fin 1`) to `a`. Essentially, this is saying that a function which orders a one-element set in terms of finite sets will always map that single element to `a`.
More concisely: For any linear order type `α` and element `a` in `α`, the function `orderEmbOfFin` maps the singleton set `{a}` to `a` in the order embedding of `Fin 1` into `α`.
|
Finset.orderEmbOfFin_zero
theorem Finset.orderEmbOfFin_zero :
∀ {α : Type u_1} [inst : LinearOrder α] {s : Finset α} {k : ℕ} (h : s.card = k) (hz : 0 < k),
(s.orderEmbOfFin h) ⟨0, hz⟩ = s.min' ⋯
This theorem, `Finset.orderEmbOfFin_zero`, states that for any type `α` with a linear order, any finite set `s` of type `α`, and any natural number `k` such that the cardinality of `s` is `k` and `k` is greater than 0, the bijection `orderEmbOfFin s h` maps the element 0 to the minimum element of `s`. The function `orderEmbOfFin s h` creates a bijective function from the set {0, ..., k-1} to `s`, and this theorem is asserting that the minimum element of this map's range is the smallest element of `s`.
More concisely: For any finite set `s` of a linearly ordered type `α` with cardinality `k > 0`, the minimum element of `s` is the image of `0` under the order embedding `orderEmbOfFin s h`.
|
Finset.mem_sort
theorem Finset.mem_sort :
∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r] [inst_2 : IsAntisymm α r]
[inst_3 : IsTotal α r] {s : Finset α} {a : α}, a ∈ Finset.sort r s ↔ a ∈ s
The theorem `Finset.mem_sort` states that for any type `α`, any decidable relation `r` on `α` that is transitive, antisymmetric and total, any finite set `s` of type `α`, and any element `a` of type `α`, `a` is an element of the sorted list of `s` (obtained using the relation `r`) if and only if `a` is an element of `s`. This theorem essentially guarantees that the sorting operation does not change the elements of the set, it only rearranges them.
More concisely: For any type `α`, decidable relation `r` on `α` that is transitive, antisymmetric and total, and finite set `s` of type `α`, the sorted list of `s` using `r` equals `s`.
|
Finset.sort_eq
theorem Finset.sort_eq :
∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r] [inst_2 : IsAntisymm α r]
[inst_3 : IsTotal α r] (s : Finset α), ↑(Finset.sort r s) = s.val
The theorem `Finset.sort_eq` states that for any type `α`, given a relation `r` on `α` that is decidable, transitive, antisymmetric, and total, and any finite set `s` of type `α`, the list of elements obtained by sorting the set `s` using `r` is exactly the multiset value of `s`. In other words, sorting a finite set under these conditions does not alter the underlying elements, it merely arranges them according to the relation `r`.
More concisely: For any decidable, transitive, antisymmetric, and total relation `r` on type `α` and finite set `s` of type `α`, the sorted list obtained using `r` is equal to the multiset of `s`.
|
Finset.orderEmbOfFin_unique'
theorem Finset.orderEmbOfFin_unique' :
∀ {α : Type u_1} [inst : LinearOrder α] {s : Finset α} {k : ℕ} (h : s.card = k) {f : Fin k ↪o α},
(∀ (x : Fin k), f x ∈ s) → f = s.orderEmbOfFin h
The theorem `Finset.orderEmbOfFin_unique'` states that for any order embedding `f` from `Fin k` (where `k` is a natural number and `Fin k` is the type of finite ordinals less than `k`) to a finite set `s` of a type `α` (with a linear ordering) of cardinality `k`, if every element `x` from `Fin k` is in `s`, then the order embedding `f` is equal to the increasing bijection `orderEmbOfFin s h` (where `h` is the proof that the cardinality of `s` is `k`). In other words, there is a unique order-preserving bijection from `Fin k` to a finite set of cardinality `k`.
More concisely: Given an order embedding from `Fin k` to a finite set `s` of cardinality `k`, if every element in `Fin k` is in `s`, then the order embedding is equal to the unique order-preserving bijection from `Fin k` to `s`.
|