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.)

Equations

• Finset.sort r s = Multiset.sort r s.val

@[simp]

theorem Finset.sort_val {α : Type u_1} (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] (s : Finset α) : Multiset.sort r s.val = Finset.sort r s

@[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 α) : (Finset.sort r s).Nodup

@[simp]

theorem Finset.sort_toFinset {α : Type u_1} (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] [DecidableEq α] (s : Finset α) : (Finset.sort r s).toFinset = 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 α} : (Finset.sort r s).length = s.card

@[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_cons {α : Type u_1} (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] {a : α} {s : Finset α} (h₁ : ∀ b ∈ s, r a b) (h₂ : a ∉ s) : Finset.sort r (Finset.cons a s h₂) = a :: Finset.sort r s

theorem Finset.sort_insert {α : Type u_1} (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] [DecidableEq α] {a : α} {s : Finset α} (h₁ : ∀ b ∈ s, r a b) (h₂ : a ∉ s) : Finset.sort r (insert a s) = a :: Finset.sort r s

theorem Finset.sort_perm_toList {α : Type u_1} (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] (s : Finset α) : (Finset.sort r s).Perm s.toList

theorem List.toFinset_sort {α : Type u_1} (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] [DecidableEq α] {l : List α} (hl : l.Nodup) : Finset.sort r l.toFinset = l ↔ List.Sorted r l

theorem Finset.sort_sorted_lt {α : Type u_1} [LinearOrder α] (s : Finset α) : List.Sorted (fun (x1 x2 : α) => x1 < x2) (Finset.sort (fun (x1 x2 : α) => x1 ≤ x2) s)

theorem Finset.sort_sorted_gt {α : Type u_1} [LinearOrder α] (s : Finset α) : List.Sorted (fun (x1 x2 : α) => x1 > x2) (Finset.sort (fun (x1 x2 : α) => x1 ≥ x2) s)

theorem Finset.sorted_zero_eq_min'_aux {α : Type u_1} [LinearOrder α] (s : Finset α) (h : 0 < (Finset.sort (fun (x1 x2 : α) => x1 ≤ x2) s).length) (H : s.Nonempty) : (Finset.sort (fun (x1 x2 : α) => x1 ≤ x2) s).get ⟨0, h⟩ = s.min' H

theorem Finset.sorted_zero_eq_min' {α : Type u_1} [LinearOrder α] {s : Finset α} {h : 0 < (Finset.sort (fun (x1 x2 : α) => x1 ≤ x2) s).length} : (Finset.sort (fun (x1 x2 : α) => x1 ≤ x2) s)[0] = s.min' ⋯

theorem Finset.min'_eq_sorted_zero {α : Type u_1} [LinearOrder α] {s : Finset α} {h : s.Nonempty} : s.min' h = (Finset.sort (fun (x1 x2 : α) => x1 ≤ x2) s)[0]

theorem Finset.sorted_last_eq_max'_aux {α : Type u_1} [LinearOrder α] (s : Finset α) (h : (Finset.sort (fun (x1 x2 : α) => x1 ≤ x2) s).length - 1 < (Finset.sort (fun (x1 x2 : α) => x1 ≤ x2) s).length) (H : s.Nonempty) : (Finset.sort (fun (x1 x2 : α) => x1 ≤ x2) s)[(Finset.sort (fun (x1 x2 : α) => x1 ≤ x2) s).length - 1] = s.max' H

theorem Finset.sorted_last_eq_max' {α : Type u_1} [LinearOrder α] {s : Finset α} {h : (Finset.sort (fun (x1 x2 : α) => x1 ≤ x2) s).length - 1 < (Finset.sort (fun (x1 x2 : α) => x1 ≤ x2) s).length} : (Finset.sort (fun (x1 x2 : α) => x1 ≤ x2) s)[(Finset.sort (fun (x1 x2 : α) => x1 ≤ x2) s).length - 1] = s.max' ⋯

theorem Finset.max'_eq_sorted_last {α : Type u_1} [LinearOrder α] {s : Finset α} {h : s.Nonempty} : s.max' h = (Finset.sort (fun (x1 x2 : α) => x1 ≤ x2) s)[(Finset.sort (fun (x1 x2 : α) => x1 ≤ x2) s).length - 1]

def Finset.orderIsoOfFin {α : Type u_1} [LinearOrder α] (s : Finset α) {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.

def Finset.orderEmbOfFin {α : Type u_1} [LinearOrder α] (s : Finset α) {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

• s.orderEmbOfFin h = RelEmbedding.trans (s.orderIsoOfFin h).toOrderEmbedding (OrderEmbedding.subtype fun (x : α) => x ∈ s)

@[simp]

theorem Finset.coe_orderIsoOfFin_apply {α : Type u_1} [LinearOrder α] (s : Finset α) {k : ℕ} (h : s.card = k) (i : Fin k) : ↑((s.orderIsoOfFin h) i) = (s.orderEmbOfFin h) i

theorem Finset.orderIsoOfFin_symm_apply {α : Type u_1} [LinearOrder α] (s : Finset α) {k : ℕ} (h : s.card = k) (x : { x : α // x ∈ s }) : ↑((s.orderIsoOfFin h).symm x) = List.indexOf (↑x) (Finset.sort (fun (x1 x2 : α) => x1 ≤ x2) s)

theorem Finset.orderEmbOfFin_apply {α : Type u_1} [LinearOrder α] (s : Finset α) {k : ℕ} (h : s.card = k) (i : Fin k) : (s.orderEmbOfFin h) i = (Finset.sort (fun (x1 x2 : α) => x1 ≤ x2) s)[i]

@[simp]

theorem Finset.orderEmbOfFin_mem {α : Type u_1} [LinearOrder α] (s : Finset α) {k : ℕ} (h : s.card = k) (i : Fin k) : (s.orderEmbOfFin h) i ∈ s

@[simp]

theorem Finset.range_orderEmbOfFin {α : Type u_1} [LinearOrder α] (s : Finset α) {k : ℕ} (h : s.card = k) : Set.range ⇑(s.orderEmbOfFin h) = ↑s

theorem Finset.orderEmbOfFin_zero {α : Type u_1} [LinearOrder α] {s : Finset α} {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} [LinearOrder α] {s : Finset α} {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} [LinearOrder α] (a : α) (i : Fin 1) : ({a}.orderEmbOfFin ⋯) i = a

orderEmbOfFin {a} h sends any argument to a.

theorem Finset.orderEmbOfFin_unique {α : Type u_1} [LinearOrder α] {s : Finset α} {k : ℕ} (h : s.card = k) {f : Fin k → α} (hfs : ∀ (x : Fin k), f x ∈ s) (hmono : StrictMono f) : 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} [LinearOrder α] {s : Finset α} {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} [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

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 ≤ 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

• s.orderEmbOfCardLe h = RelEmbedding.trans (Fin.castLEOrderEmb h) (s.orderEmbOfFin ⋯)

theorem Finset.orderEmbOfCardLe_mem {α : Type u_1} [LinearOrder α] (s : Finset α) {k : ℕ} (h : k ≤ s.card) (a : Fin k) : (s.orderEmbOfCardLe h) a ∈ s

unsafe instance Finset.instRepr {α : Type u_1} [Repr α] : Repr (Finset α)

theorem Fin.sort_univ (n : ℕ) : Finset.sort (fun (x y : Fin n) => x ≤ y) Finset.univ = List.finRange n

def Fintype.orderIsoFinOfCardEq (α : Type u_1) [LinearOrder α] [Fintype α] {k : ℕ} (h : Fintype.card α = k) : Fin k ≃o α

Given a Fintype α of cardinality k, the map orderIsoFinOfCardEq s h is the increasing bijection between Fin k and α as an OrderIso. Here, h is a proof that the cardinality of α is k. We use this instead of an iso Fin (Fintype.card α) ≃o α to avoid casting issues in further uses of this function.

Equations

• Fintype.orderIsoFinOfCardEq α h = (Finset.univ.orderIsoOfFin h).trans ((OrderIso.setCongr (↑Finset.univ) Set.univ ⋯).trans OrderIso.Set.univ)

theorem nonempty_orderEmbedding_of_finite_infinite (α : Type u_1) [LinearOrder α] [hα : Finite α] (β : Type u_2) [LinearOrder β] [hβ : Infinite β] : Nonempty (α ↪o β)

Any finite linear order order-embeds into any infinite linear order.