mathlib docs: data.finset.sort

def finset.sort {α : Type u_1} (r : α → α → Prop) [decidable_rel r] [is_trans α r] [is_antisymm α r] [is_total α r] :

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_sorted {α : Type u_1} (r : α → α → Prop) [decidable_rel r] [is_trans α r] [is_antisymm α r] [is_total α r] (s : finset α) :

list.sorted r (finset.sort r s)

source

@[simp]

theorem finset.sort_eq {α : Type u_1} (r : α → α → Prop) [decidable_rel r] [is_trans α r] [is_antisymm α r] [is_total α r] (s : finset α) :

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

source

@[simp]

theorem finset.sort_nodup {α : Type u_1} (r : α → α → Prop) [decidable_rel r] [is_trans α r] [is_antisymm α r] [is_total α r] (s : finset α) :

(finset.sort r s).nodup

source

@[simp]

theorem finset.sort_to_finset {α : Type u_1} (r : α → α → Prop) [decidable_rel r] [is_trans α r] [is_antisymm α r] [is_total α r] [decidable_eq α] (s : finset α) :

(finset.sort r s).to_finset = s

source

@[simp]

theorem finset.mem_sort {α : Type u_1} (r : α → α → Prop) [decidable_rel r] [is_trans α r] [is_antisymm α r] [is_total α r] {s : finset α} {a : α} :

a ∈ finset.sort r s ↔ a ∈ s

source

@[simp]

theorem finset.length_sort {α : Type u_1} (r : α → α → Prop) [decidable_rel r] [is_trans α r] [is_antisymm α r] [is_total α r] {s : finset α} :

(finset.sort r s).length = s.card

source

theorem finset.sort_sorted_lt {α : Type u_1} [decidable_linear_order α] (s : finset α) :

list.sorted has_lt.lt (finset.sort has_le.le s)

source

theorem finset.sorted_zero_eq_min' {α : Type u_1} [decidable_linear_order α] (s : finset α) (h : 0 < (finset.sort has_le.le s).length) (H : s.nonempty) :

(finset.sort has_le.le s).nth_le 0 h = s.min' H

source

theorem finset.sorted_last_eq_max' {α : Type u_1} [decidable_linear_order α] (s : finset α) (h : (finset.sort has_le.le s).length - 1 < (finset.sort has_le.le s).length) (H : s.nonempty) :

(finset.sort has_le.le s).nth_le ((finset.sort has_le.le s).length - 1) h = s.max' H

source

def finset.mono_of_fin {α : Type u_1} [decidable_linear_order α] (s : finset α) {k : ℕ} :

s.card = k → fin k → α

Given a finset s of cardinal k in a linear order α, the map mono_of_fin s h is the increasing bijection between fin k and s as an α-valued map. Here, h is a proof that the cardinality of s is k. We use this instead of a map fin s.card → α to avoid casting issues in further uses of this function.

Equations

s.mono_of_fin h i = have A : ↑i < (finset.sort has_le.le s).length, from _, (finset.sort has_le.le s).nth_le ↑i A

source

theorem finset.mono_of_fin_strict_mono {α : Type u_1} [decidable_linear_order α] (s : finset α) {k : ℕ} (h : s.card = k) :

strict_mono (s.mono_of_fin h)

source

theorem finset.mono_of_fin_bij_on {α : Type u_1} [decidable_linear_order α] (s : finset α) {k : ℕ} (h : s.card = k) :

set.bij_on (s.mono_of_fin h) set.univ ↑s

source

theorem finset.mono_of_fin_injective {α : Type u_1} [decidable_linear_order α] (s : finset α) {k : ℕ} (h : s.card = k) :

function.injective (s.mono_of_fin h)

source

theorem finset.mono_of_fin_zero {α : Type u_1} [decidable_linear_order α] {s : finset α} {k : ℕ} (h : s.card = k) (hs : s.nonempty) (hz : 0 < k) :

s.mono_of_fin h ⟨0, hz⟩ = s.min' hs

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

source

theorem finset.mono_of_fin_last {α : Type u_1} [decidable_linear_order α] {s : finset α} {k : ℕ} (h : s.card = k) (hs : s.nonempty) (hz : 0 < k) :

s.mono_of_fin h ⟨k - 1, _⟩ = s.max' hs

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

source

@[simp]

theorem finset.mono_of_fin_singleton {α : Type u_1} [decidable_linear_order α] (a : α) (i : fin 1) {h : {a}.card = 1} :

{a}.mono_of_fin h i = a

mono_of_fin {a} h sends any argument to a.

source

theorem finset.mono_of_fin_unique {α : Type u_1} [decidable_linear_order α] {s : finset α} {k : ℕ} (h : s.card = k) {f : fin k → α} :

set.bij_on f set.univ ↑s → strict_mono f → f = s.mono_of_fin h

Any increasing bijection between fin k and a finset of cardinality k has to coincide with the increasing bijection mono_of_fin s h. For a statement assuming only that f maps univ to s, see mono_of_fin_unique'.

source

theorem finset.mono_of_fin_unique' {α : Type u_1} [decidable_linear_order α] {s : finset α} {k : ℕ} (h : s.card = k) {f : fin k → α} :

set.maps_to f set.univ ↑s → strict_mono f → f = s.mono_of_fin h

Any increasing map between fin k and a finset of cardinality k has to coincide with the increasing bijection mono_of_fin s h.

source

@[simp]

theorem finset.mono_of_fin_eq_mono_of_fin_iff {α : Type u_1} [decidable_linear_order α] {k l : ℕ} {s : finset α} {i : fin k} {j : fin l} {h : s.card = k} {h' : s.card = l} :

s.mono_of_fin h i = s.mono_of_fin h' j ↔ i.val = j.val

Two parametrizations mono_of_fin 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.val = j.val.

source

def finset.mono_equiv_of_fin {α : Type u_1} [decidable_linear_order α] (s : finset α) {k : ℕ} :

s.card = k → fin k ≃ {x // x ∈ s}

Given a finset s of cardinal k in a linear order α, the equiv mono_equiv_of_fin s h is the increasing bijection between fin k and s as an s-valued map. Here, h is a proof that the cardinality of s is k. We use this instead of a map fin s.card → α to avoid casting issues in further uses of this function.