Construct a sorted list from a finset. #
sort #
def
Finset.sort
{α : Type u_1}
(r : α → α → Prop)
[DecidableRel r]
[IsTrans α r]
[IsAntisymm α r]
[IsTotal α r]
(s : Finset α)
:
List α
sort s constructs a sorted list from the unordered set s.
(Uses merge sort algorithm.)
Instances For
@[simp]
theorem
Finset.sort_sorted
{α : Type u_1}
(r : α → α → Prop)
[DecidableRel r]
[IsTrans α r]
[IsAntisymm α r]
[IsTotal α r]
(s : Finset α)
:
List.Sorted r (Finset.sort r s)
@[simp]
theorem
Finset.sort_eq
{α : Type u_1}
(r : α → α → Prop)
[DecidableRel r]
[IsTrans α r]
[IsAntisymm α r]
[IsTotal α r]
(s : Finset α)
:
↑(Finset.sort r s) = s.val
@[simp]
theorem
Finset.sort_nodup
{α : Type u_1}
(r : α → α → Prop)
[DecidableRel r]
[IsTrans α r]
[IsAntisymm α r]
[IsTotal α r]
(s : Finset α)
:
List.Nodup (Finset.sort r s)
@[simp]
theorem
Finset.sort_toFinset
{α : Type u_1}
(r : α → α → Prop)
[DecidableRel r]
[IsTrans α r]
[IsAntisymm α r]
[IsTotal α r]
[DecidableEq α]
(s : Finset α)
:
List.toFinset (Finset.sort r s) = s
@[simp]
theorem
Finset.mem_sort
{α : Type u_1}
(r : α → α → Prop)
[DecidableRel r]
[IsTrans α r]
[IsAntisymm α r]
[IsTotal α r]
{s : Finset α}
{a : α}
:
a ∈ Finset.sort r s ↔ a ∈ s
@[simp]
theorem
Finset.length_sort
{α : Type u_1}
(r : α → α → Prop)
[DecidableRel r]
[IsTrans α r]
[IsAntisymm α r]
[IsTotal α r]
{s : Finset α}
:
List.length (Finset.sort r s) = Finset.card s
@[simp]
theorem
Finset.sort_empty
{α : Type u_1}
(r : α → α → Prop)
[DecidableRel r]
[IsTrans α r]
[IsAntisymm α r]
[IsTotal α r]
:
Finset.sort r ∅ = []
@[simp]
theorem
Finset.sort_singleton
{α : Type u_1}
(r : α → α → Prop)
[DecidableRel r]
[IsTrans α r]
[IsAntisymm α r]
[IsTotal α r]
(a : α)
:
Finset.sort r {a} = [a]
theorem
Finset.sort_perm_toList
{α : Type u_1}
(r : α → α → Prop)
[DecidableRel r]
[IsTrans α r]
[IsAntisymm α r]
[IsTotal α r]
(s : Finset α)
:
Finset.sort r s ~ Finset.toList s
theorem
Finset.sort_sorted_lt
{α : Type u_1}
[LinearOrder α]
(s : Finset α)
:
List.Sorted (fun x x_1 => x < x_1) (Finset.sort (fun x x_1 => x ≤ x_1) s)
theorem
Finset.sorted_zero_eq_min'_aux
{α : Type u_1}
[LinearOrder α]
(s : Finset α)
(h : 0 < List.length (Finset.sort (fun x x_1 => x ≤ x_1) s))
(H : Finset.Nonempty s)
:
List.nthLe (Finset.sort (fun x x_1 => x ≤ x_1) s) 0 h = Finset.min' s H
theorem
Finset.sorted_zero_eq_min'
{α : Type u_1}
[LinearOrder α]
{s : Finset α}
{h : 0 < List.length (Finset.sort (fun x x_1 => x ≤ x_1) s)}
:
List.nthLe (Finset.sort (fun x x_1 => x ≤ x_1) s) 0 h = Finset.min' s (_ : Finset.Nonempty s)
theorem
Finset.min'_eq_sorted_zero
{α : Type u_1}
[LinearOrder α]
{s : Finset α}
{h : Finset.Nonempty s}
:
Finset.min' s h = List.nthLe (Finset.sort (fun x x_1 => x ≤ x_1) s) 0 (_ : 0 < List.length (Finset.sort (fun x x_1 => x ≤ x_1) s))
theorem
Finset.sorted_last_eq_max'_aux
{α : Type u_1}
[LinearOrder α]
(s : Finset α)
(h : List.length (Finset.sort (fun x x_1 => x ≤ x_1) s) - 1 < List.length (Finset.sort (fun x x_1 => x ≤ x_1) s))
(H : Finset.Nonempty s)
:
List.nthLe (Finset.sort (fun x x_1 => x ≤ x_1) s) (List.length (Finset.sort (fun x x_1 => x ≤ x_1) s) - 1) h = Finset.max' s H
theorem
Finset.sorted_last_eq_max'
{α : Type u_1}
[LinearOrder α]
{s : Finset α}
{h : List.length (Finset.sort (fun x x_1 => x ≤ x_1) s) - 1 < List.length (Finset.sort (fun x x_1 => x ≤ x_1) s)}
:
List.nthLe (Finset.sort (fun x x_1 => x ≤ x_1) s) (List.length (Finset.sort (fun x x_1 => x ≤ x_1) s) - 1) h = Finset.max' s (_ : Finset.Nonempty s)
theorem
Finset.max'_eq_sorted_last
{α : Type u_1}
[LinearOrder α]
{s : Finset α}
{h : Finset.Nonempty s}
:
Finset.max' s h = List.nthLe (Finset.sort (fun x x_1 => x ≤ x_1) s) (List.length (Finset.sort (fun x x_1 => x ≤ x_1) s) - 1)
(_ : List.length (Finset.sort (fun x x_1 => x ≤ x_1) s) - 1 < List.length (Finset.sort (fun x x_1 => x ≤ x_1) s))
def
Finset.orderIsoOfFin
{α : Type u_1}
[LinearOrder α]
(s : Finset α)
{k : ℕ}
(h : Finset.card s = k)
:
Given a finset s of cardinality k in a linear order α, the map orderIsoOfFin s h
is the increasing bijection between Fin k and s as an OrderIso. Here, h is a proof that
the cardinality of s is k. We use this instead of an iso Fin s.card ≃o s to avoid
casting issues in further uses of this function.
Instances For
def
Finset.orderEmbOfFin
{α : Type u_1}
[LinearOrder α]
(s : Finset α)
{k : ℕ}
(h : Finset.card s = k)
:
Given a finset s of cardinality k in a linear order α, the map orderEmbOfFin s h is
the increasing bijection between Fin k and s as an order embedding into α. Here, h is a
proof that the cardinality of s is k. We use this instead of an embedding Fin s.card ↪o α to
avoid casting issues in further uses of this function.
Instances For
@[simp]
theorem
Finset.coe_orderIsoOfFin_apply
{α : Type u_1}
[LinearOrder α]
(s : Finset α)
{k : ℕ}
(h : Finset.card s = k)
(i : Fin k)
:
↑(↑(Finset.orderIsoOfFin s h) i) = ↑(Finset.orderEmbOfFin s h) i
theorem
Finset.orderIsoOfFin_symm_apply
{α : Type u_1}
[LinearOrder α]
(s : Finset α)
{k : ℕ}
(h : Finset.card s = k)
(x : { x // x ∈ s })
:
↑(↑(OrderIso.symm (Finset.orderIsoOfFin s h)) x) = List.indexOf (↑x) (Finset.sort (fun x x_1 => x ≤ x_1) s)
theorem
Finset.orderEmbOfFin_apply
{α : Type u_1}
[LinearOrder α]
(s : Finset α)
{k : ℕ}
(h : Finset.card s = k)
(i : Fin k)
:
↑(Finset.orderEmbOfFin s h) i = List.nthLe (Finset.sort (fun x x_1 => x ≤ x_1) s) ↑i (_ : ↑i < List.length (Finset.sort (fun x x_1 => x ≤ x_1) s))
@[simp]
theorem
Finset.orderEmbOfFin_mem
{α : Type u_1}
[LinearOrder α]
(s : Finset α)
{k : ℕ}
(h : Finset.card s = k)
(i : Fin k)
:
↑(Finset.orderEmbOfFin s h) i ∈ s
@[simp]
theorem
Finset.range_orderEmbOfFin
{α : Type u_1}
[LinearOrder α]
(s : Finset α)
{k : ℕ}
(h : Finset.card s = k)
:
Set.range ↑(Finset.orderEmbOfFin s h) = ↑s
theorem
Finset.orderEmbOfFin_zero
{α : Type u_1}
[LinearOrder α]
{s : Finset α}
{k : ℕ}
(h : Finset.card s = k)
(hz : 0 < k)
:
↑(Finset.orderEmbOfFin s h) { val := 0, isLt := hz } = Finset.min' s (_ : Finset.Nonempty s)
The bijection orderEmbOfFin s h sends 0 to the minimum of s.
theorem
Finset.orderEmbOfFin_last
{α : Type u_1}
[LinearOrder α]
{s : Finset α}
{k : ℕ}
(h : Finset.card s = k)
(hz : 0 < k)
:
↑(Finset.orderEmbOfFin s h) { val := k - 1, isLt := (_ : k - 1 < k) } = Finset.max' s (_ : Finset.Nonempty s)
The bijection orderEmbOfFin s h sends k-1 to the maximum of s.
@[simp]
theorem
Finset.orderEmbOfFin_singleton
{α : Type u_1}
[LinearOrder α]
(a : α)
(i : Fin 1)
:
↑(Finset.orderEmbOfFin {a} (_ : Finset.card {a} = 1)) i = a
orderEmbOfFin {a} h sends any argument to a.
theorem
Finset.orderEmbOfFin_unique
{α : Type u_1}
[LinearOrder α]
{s : Finset α}
{k : ℕ}
(h : Finset.card s = k)
{f : Fin k → α}
(hfs : ∀ (x : Fin k), f x ∈ s)
(hmono : StrictMono f)
:
f = ↑(Finset.orderEmbOfFin s h)
Any increasing map f from Fin k to a finset of cardinality k has to coincide with
the increasing bijection orderEmbOfFin s h.
theorem
Finset.orderEmbOfFin_unique'
{α : Type u_1}
[LinearOrder α]
{s : Finset α}
{k : ℕ}
(h : Finset.card s = k)
{f : Fin k ↪o α}
(hfs : ∀ (x : Fin k), ↑f x ∈ s)
:
f = Finset.orderEmbOfFin s h
An order embedding f from Fin k to a finset of cardinality k has to coincide with
the increasing bijection orderEmbOfFin s h.
@[simp]
theorem
Finset.orderEmbOfFin_eq_orderEmbOfFin_iff
{α : Type u_1}
[LinearOrder α]
{k : ℕ}
{l : ℕ}
{s : Finset α}
{i : Fin k}
{j : Fin l}
{h : Finset.card s = k}
{h' : Finset.card s = l}
:
↑(Finset.orderEmbOfFin s h) i = ↑(Finset.orderEmbOfFin s h') j ↔ ↑i = ↑j
Two parametrizations orderEmbOfFin of the same set take the same value on i and j if
and only if i = j. Since they can be defined on a priori not defeq types Fin k and Fin l
(although necessarily k = l), the conclusion is rather written (i : ℕ) = (j : ℕ).
def
Finset.orderEmbOfCardLe
{α : Type u_1}
[LinearOrder α]
(s : Finset α)
{k : ℕ}
(h : k ≤ Finset.card s)
:
Given a finset s of size at least k in a linear order α, the map orderEmbOfCardLe
is an order embedding from Fin k to α whose image is contained in s. Specifically, it maps
Fin k to an initial segment of s.
Instances For
theorem
Finset.orderEmbOfCardLe_mem
{α : Type u_1}
[LinearOrder α]
(s : Finset α)
{k : ℕ}
(h : k ≤ Finset.card s)
(a : Fin k)
:
↑(Finset.orderEmbOfCardLe s h) a ∈ s