# Construct a sorted list from a finset. #

### sort #

def Finset.sort {α : Type u_1} (r : ααProp) [] [IsTrans α r] [] [IsTotal α r] (s : ) :
List α

sort s constructs a sorted list from the unordered set s. (Uses merge sort algorithm.)

Equations
Instances For
@[simp]
theorem Finset.sort_sorted {α : Type u_1} (r : ααProp) [] [IsTrans α r] [] [IsTotal α r] (s : ) :
@[simp]
theorem Finset.sort_eq {α : Type u_1} (r : ααProp) [] [IsTrans α r] [] [IsTotal α r] (s : ) :
() = s.val
@[simp]
theorem Finset.sort_nodup {α : Type u_1} (r : ααProp) [] [IsTrans α r] [] [IsTotal α r] (s : ) :
().Nodup
@[simp]
theorem Finset.sort_toFinset {α : Type u_1} (r : ααProp) [] [IsTrans α r] [] [IsTotal α r] [] (s : ) :
().toFinset = s
@[simp]
theorem Finset.mem_sort {α : Type u_1} (r : ααProp) [] [IsTrans α r] [] [IsTotal α r] {s : } {a : α} :
a a s
@[simp]
theorem Finset.length_sort {α : Type u_1} (r : ααProp) [] [IsTrans α r] [] [IsTotal α r] {s : } :
().length = s.card
@[simp]
theorem Finset.sort_empty {α : Type u_1} (r : ααProp) [] [IsTrans α r] [] [IsTotal α r] :
= []
@[simp]
theorem Finset.sort_singleton {α : Type u_1} (r : ααProp) [] [IsTrans α r] [] [IsTotal α r] (a : α) :
Finset.sort r {a} = [a]
theorem Finset.sort_perm_toList {α : Type u_1} (r : ααProp) [] [IsTrans α r] [] [IsTotal α r] (s : ) :
().Perm s.toList
theorem Finset.sort_sorted_lt {α : Type u_1} [] (s : ) :
List.Sorted (fun (x x_1 : α) => x < x_1) (Finset.sort (fun (x x_1 : α) => x x_1) s)
theorem Finset.sort_sorted_gt {α : Type u_1} [] (s : ) :
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} [] (s : ) (h : 0 < (Finset.sort (fun (x x_1 : α) => x x_1) s).length) (H : s.Nonempty) :
(Finset.sort (fun (x x_1 : α) => x x_1) s).get 0, h = s.min' H
theorem Finset.sorted_zero_eq_min' {α : Type u_1} [] {s : } {h : 0 < (Finset.sort (fun (x x_1 : α) => x x_1) s).length} :
(Finset.sort (fun (x x_1 : α) => x x_1) s).get 0, h = s.min'
theorem Finset.min'_eq_sorted_zero {α : Type u_1} [] {s : } {h : s.Nonempty} :
s.min' h = (Finset.sort (fun (x x_1 : α) => x x_1) s).get 0,
theorem Finset.sorted_last_eq_max'_aux {α : Type u_1} [] (s : ) (h : (Finset.sort (fun (x x_1 : α) => x x_1) s).length - 1 < (Finset.sort (fun (x x_1 : α) => x x_1) s).length) (H : s.Nonempty) :
(Finset.sort (fun (x x_1 : α) => x x_1) s).get (Finset.sort (fun (x x_1 : α) => x x_1) s).length - 1, h = s.max' H
theorem Finset.sorted_last_eq_max' {α : Type u_1} [] {s : } {h : (Finset.sort (fun (x x_1 : α) => x x_1) s).length - 1 < (Finset.sort (fun (x x_1 : α) => x x_1) s).length} :
(Finset.sort (fun (x x_1 : α) => x x_1) s).get (Finset.sort (fun (x x_1 : α) => x x_1) s).length - 1, h = s.max'
theorem Finset.max'_eq_sorted_last {α : Type u_1} [] {s : } {h : s.Nonempty} :
s.max' h = (Finset.sort (fun (x x_1 : α) => x x_1) s).get (Finset.sort (fun (x x_1 : α) => x x_1) s).length - 1,
def Finset.orderIsoOfFin {α : Type u_1} [] (s : ) {k : } (h : s.card = k) :
Fin k ≃o { x : α // x s }

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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Finset.orderEmbOfFin {α : Type u_1} [] (s : ) {k : } (h : s.card = k) :
Fin k ↪o α

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.

Equations
Instances For
@[simp]
theorem Finset.coe_orderIsoOfFin_apply {α : Type u_1} [] (s : ) {k : } (h : s.card = k) (i : Fin k) :
((s.orderIsoOfFin h) i) = (s.orderEmbOfFin h) i
theorem Finset.orderIsoOfFin_symm_apply {α : Type u_1} [] (s : ) {k : } (h : s.card = k) (x : { x : α // x s }) :
((s.orderIsoOfFin h).symm x) = List.indexOf (x) (Finset.sort (fun (x x_1 : α) => x x_1) s)
theorem Finset.orderEmbOfFin_apply {α : Type u_1} [] (s : ) {k : } (h : s.card = k) (i : Fin k) :
(s.orderEmbOfFin h) i = (Finset.sort (fun (x x_1 : α) => x x_1) s).get i,
@[simp]
theorem Finset.orderEmbOfFin_mem {α : Type u_1} [] (s : ) {k : } (h : s.card = k) (i : Fin k) :
(s.orderEmbOfFin h) i s
@[simp]
theorem Finset.range_orderEmbOfFin {α : Type u_1} [] (s : ) {k : } (h : s.card = k) :
Set.range (s.orderEmbOfFin h) = s
theorem Finset.orderEmbOfFin_zero {α : Type u_1} [] {s : } {k : } (h : s.card = k) (hz : 0 < k) :
(s.orderEmbOfFin h) 0, hz = s.min'

The bijection orderEmbOfFin s h sends 0 to the minimum of s.

theorem Finset.orderEmbOfFin_last {α : Type u_1} [] {s : } {k : } (h : s.card = k) (hz : 0 < k) :
(s.orderEmbOfFin h) k - 1, = s.max'

The bijection orderEmbOfFin s h sends k-1 to the maximum of s.

@[simp]
theorem Finset.orderEmbOfFin_singleton {α : Type u_1} [] (a : α) (i : Fin 1) :
({a}.orderEmbOfFin ) i = a

orderEmbOfFin {a} h sends any argument to a.

theorem Finset.orderEmbOfFin_unique {α : Type u_1} [] {s : } {k : } (h : s.card = k) {f : Fin kα} (hfs : ∀ (x : Fin k), f x s) (hmono : ) :
f = (s.orderEmbOfFin 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} [] {s : } {k : } (h : s.card = k) {f : Fin k ↪o α} (hfs : ∀ (x : Fin k), f x s) :
f = s.orderEmbOfFin 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} [] {k : } {l : } {s : } {i : Fin k} {j : Fin l} {h : s.card = k} {h' : s.card = l} :
(s.orderEmbOfFin h) i = (s.orderEmbOfFin 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} [] (s : ) {k : } (h : k s.card) :
Fin k ↪o α

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.

Equations
Instances For
theorem Finset.orderEmbOfCardLe_mem {α : Type u_1} [] (s : ) {k : } (h : k s.card) (a : Fin k) :
(s.orderEmbOfCardLe h) a s
unsafe instance Finset.instRepr {α : Type u_1} [Repr α] :
Repr ()
Equations
• Finset.instRepr = { reprPrec := fun (s : ) (x : ) => if s.card = 0 then else repr s.val }
theorem Fin.sort_univ (n : ) :
Finset.sort (fun (x y : Fin n) => x y) Finset.univ =