Construct a sorted list from a finset. #

sort #

def Finset.sort {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] [inst : IsTrans α r] [inst : IsAntisymm α r] [inst : 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

source

ink

@[simp]

theorem Finset.sort_sorted {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] [inst : IsTrans α r] [inst : IsAntisymm α r] [inst : IsTotal α r] (s : Finset α) :

List.Sorted r (Finset.sort r s)

source

ink

@[simp]

theorem Finset.sort_eq {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] [inst : IsTrans α r] [inst : IsAntisymm α r] [inst : IsTotal α r] (s : Finset α) :

↑(Finset.sort r s) = s.val

source

ink

@[simp]

theorem Finset.sort_nodup {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] [inst : IsTrans α r] [inst : IsAntisymm α r] [inst : IsTotal α r] (s : Finset α) :

List.Nodup (Finset.sort r s)

source

ink

@[simp]

theorem Finset.sort_toFinset {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] [inst : IsTrans α r] [inst : IsAntisymm α r] [inst : IsTotal α r] [inst : DecidableEq α] (s : Finset α) :

List.toFinset (Finset.sort r s) = s

source

ink

@[simp]

theorem Finset.mem_sort {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] [inst : IsTrans α r] [inst : IsAntisymm α r] [inst : IsTotal α r] {s : Finset α} {a : α} :

a ∈ Finset.sort r s ↔ a ∈ s

source

ink

@[simp]

theorem Finset.length_sort {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] [inst : IsTrans α r] [inst : IsAntisymm α r] [inst : IsTotal α r] {s : Finset α} :

List.length (Finset.sort r s) = Finset.card s

source

ink

@[simp]

theorem Finset.sort_empty {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] [inst : IsTrans α r] [inst : IsAntisymm α r] [inst : IsTotal α r] :

Finset.sort r ∅ = []

source

ink

@[simp]

theorem Finset.sort_singleton {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] [inst : IsTrans α r] [inst : IsAntisymm α r] [inst : IsTotal α r] (a : α) :

Finset.sort r {a} = [a]

source

ink

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

Finset.sort r s ~ Finset.toList s

source

ink

theorem Finset.sort_sorted_lt {α : Type u_1} [inst : LinearOrder α] (s : Finset α) :

List.Sorted (fun x x_1 => x < x_1) (Finset.sort (fun x x_1 => x ≤ x_1) s)

source

ink

theorem Finset.sorted_zero_eq_min'_aux {α : Type u_1} [inst : 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

source

ink

theorem Finset.sorted_zero_eq_min' {α : Type u_1} [inst : 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)

source

ink

theorem Finset.min'_eq_sorted_zero {α : Type u_1} [inst : 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))

source

ink

theorem Finset.sorted_last_eq_max'_aux {α : Type u_1} [inst : 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

source

ink

theorem Finset.sorted_last_eq_max' {α : Type u_1} [inst : 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)

source

ink

theorem Finset.max'_eq_sorted_last {α : Type u_1} [inst : 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))

source

ink

def Finset.orderIsoOfFin {α : Type u_1} [inst : LinearOrder α] (s : Finset α) {k : ℕ} (h : Finset.card s = 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≃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.

source

ink

def Finset.orderEmbOfFin {α : Type u_1} [inst : LinearOrder α] (s : Finset α) {k : ℕ} (h : Finset.card s = 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 α↪o α to avoid casting issues in further uses of this function.

Equations

Finset.orderEmbOfFin s h = RelEmbedding.trans (OrderIso.toOrderEmbedding (Finset.orderIsoOfFin s h)) (OrderEmbedding.subtype fun x => x ∈ s)

source

ink

@[simp]

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

↑(↑(RelIso.toRelEmbedding (Finset.orderIsoOfFin s h)).toEmbedding i) = ↑(Finset.orderEmbOfFin s h).toEmbedding i

source

ink

theorem Finset.orderIsoOfFin_symm_apply {α : Type u_1} [inst : LinearOrder α] (s : Finset α) {k : ℕ} (h : Finset.card s = k) (x : { x // x ∈ s }) :

↑(↑(RelIso.toRelEmbedding (OrderIso.symm (Finset.orderIsoOfFin s h))).toEmbedding x) = List.indexOf (↑x) (Finset.sort (fun x x_1 => x ≤ x_1) s)

source

ink

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

↑(Finset.orderEmbOfFin s h).toEmbedding 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))

source

ink

@[simp]

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

↑(Finset.orderEmbOfFin s h).toEmbedding i ∈ s

source

ink

@[simp]

theorem Finset.range_orderEmbOfFin {α : Type u_1} [inst : LinearOrder α] (s : Finset α) {k : ℕ} (h : Finset.card s = k) :

Set.range ↑(Finset.orderEmbOfFin s h).toEmbedding = ↑s

source

ink

theorem Finset.orderEmbOfFin_zero {α : Type u_1} [inst : LinearOrder α] {s : Finset α} {k : ℕ} (h : Finset.card s = k) (hz : 0 < k) :

↑(Finset.orderEmbOfFin s h).toEmbedding { val := 0, isLt := hz } = Finset.min' s (_ : Finset.Nonempty s)

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

source

ink

theorem Finset.orderEmbOfFin_last {α : Type u_1} [inst : LinearOrder α] {s : Finset α} {k : ℕ} (h : Finset.card s = k) (hz : 0 < k) :

↑(Finset.orderEmbOfFin s h).toEmbedding { 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.

source

ink

@[simp]

theorem Finset.orderEmbOfFin_singleton {α : Type u_1} [inst : LinearOrder α] (a : α) (i : Fin 1) :

↑(Finset.orderEmbOfFin {a} (_ : Finset.card {a} = 1)).toEmbedding i = a

orderEmbOfFin {a} h sends any argument to a.

source

ink

theorem Finset.orderEmbOfFin_unique {α : Type u_1} [inst : 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).toEmbedding

Any increasing map f from Fin k to a finset of cardinality k has to coincide with the increasing bijection orderEmbOfFin s h.

source

ink

theorem Finset.orderEmbOfFin_unique' {α : Type u_1} [inst : LinearOrder α] {s : Finset α} {k : ℕ} (h : Finset.card s = k) {f : Fin k ↪o α} (hfs : ∀ (x : Fin k), ↑f.toEmbedding 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.

source

ink

@[simp]

theorem Finset.orderEmbOfFin_eq_orderEmbOfFin_iff {α : Type u_1} [inst : 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).toEmbedding i = ↑(Finset.orderEmbOfFin s h').toEmbedding 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 : ℕ).

source

ink

def Finset.orderEmbOfCardLe {α : Type u_1} [inst : LinearOrder α] (s : Finset α) {k : ℕ} (h : k ≤ Finset.card s) :

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

Finset.orderEmbOfCardLe s h = RelEmbedding.trans (Fin.castLe h) (Finset.orderEmbOfFin s (_ : Finset.card s = Finset.card s))

source

ink

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

↑(Finset.orderEmbOfCardLe s h).toEmbedding a ∈ s

source

ink

unsafe instance Finset.instReprFinset {α : Type u_1} [inst : Repr α] :

Repr (Finset α)

Equations

Finset.instReprFinset = { reprPrec := fun s x => repr s.val }