mathlib3 documentation

data.finset.sort

Construct a sorted list from a finset. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

sort #

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

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

Equations
source
@[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
@[simp]
theorem finset.sort_empty {α : Type u_1} (r : α → α → Prop) [decidable_rel r] [is_trans α r] [is_antisymm α r] [is_total α r] :
finset.sort r ∅ = list.nil
source
@[simp]
theorem finset.sort_singleton {α : Type u_1} (r : α → α → Prop) [decidable_rel r] [is_trans α r] [is_antisymm α r] [is_total α r] (a : α) :
finset.sort r {a} = [a]
source
theorem finset.sort_perm_to_list {α : Type u_1} (r : α → α → Prop) [decidable_rel r] [is_trans α r] [is_antisymm α r] [is_total α r] (s : finset α) :
finset.sort r s ~ s.to_list
source
theorem finset.sort_sorted_lt {α : Type u_1} [linear_order α] (s : finset α) :
list.sorted has_lt.lt (finset.sort has_le.le s)
source
theorem finset.sorted_zero_eq_min'_aux {α : Type u_1} [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_zero_eq_min' {α : Type u_1} [linear_order α] {s : finset α} {h : 0 < (finset.sort has_le.le s).length} :
(finset.sort has_le.le s).nth_le 0 h = s.min' _
source
theorem finset.min'_eq_sorted_zero {α : Type u_1} [linear_order α] {s : finset α} {h : s.nonempty} :
s.min' h = (finset.sort has_le.le s).nth_le 0 _
source
theorem finset.sorted_last_eq_max'_aux {α : Type u_1} [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
theorem finset.sorted_last_eq_max' {α : Type u_1} [linear_order α] {s : finset α} {h : (finset.sort has_le.le s).length - 1 < (finset.sort has_le.le s).length} :
(finset.sort has_le.le s).nth_le ((finset.sort has_le.le s).length - 1) h = s.max' _
source
theorem finset.max'_eq_sorted_last {α : Type u_1} [linear_order α] {s : finset α} {h : s.nonempty} :
s.max' h = (finset.sort has_le.le s).nth_le ((finset.sort has_le.le s).length - 1) _
source
def finset.order_iso_of_fin {α : Type u_1} [linear_order α] (s : finset α) {k : ℕ} (h : s.card = k) :
fin k ≃o ↥s

Given a finset s of cardinality k in a linear order α, the map order_iso_of_fin s h is the increasing bijection between fin k and s as an order_iso. 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
source
def finset.order_emb_of_fin {α : Type u_1} [linear_order α] (s : finset α) {k : ℕ} (h : s.card = k) :
fin k ↪o α

Given a finset s of cardinality k in a linear order α, the map order_emb_of_fin 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
source
@[simp]
theorem finset.coe_order_iso_of_fin_apply {α : Type u_1} [linear_order α] (s : finset α) {k : ℕ} (h : s.card = k) (i : fin k) :
↑(⇑(s.order_iso_of_fin h) i) = ⇑(s.order_emb_of_fin h) i
source
theorem finset.order_iso_of_fin_symm_apply {α : Type u_1} [linear_order α] (s : finset α) {k : ℕ} (h : s.card = k) (x : ↥s) :
↑(⇑((s.order_iso_of_fin h).symm) x) = list.index_of ↑x (finset.sort has_le.le s)
source
theorem finset.order_emb_of_fin_apply {α : Type u_1} [linear_order α] (s : finset α) {k : ℕ} (h : s.card = k) (i : fin k) :
⇑(s.order_emb_of_fin h) i = (finset.sort has_le.le s).nth_le ↑i _
source
@[simp]
theorem finset.order_emb_of_fin_mem {α : Type u_1} [linear_order α] (s : finset α) {k : ℕ} (h : s.card = k) (i : fin k) :
⇑(s.order_emb_of_fin h) i ∈ s
source
@[simp]
theorem finset.range_order_emb_of_fin {α : Type u_1} [linear_order α] (s : finset α) {k : ℕ} (h : s.card = k) :
set.range ⇑(s.order_emb_of_fin h) = ↑s
source
theorem finset.order_emb_of_fin_zero {α : Type u_1} [linear_order α] {s : finset α} {k : ℕ} (h : s.card = k) (hz : 0 < k) :
⇑(s.order_emb_of_fin h) ⟨0, hz⟩ = s.min' _

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

source
theorem finset.order_emb_of_fin_last {α : Type u_1} [linear_order α] {s : finset α} {k : ℕ} (h : s.card = k) (hz : 0 < k) :
⇑(s.order_emb_of_fin h) ⟨k - 1, _⟩ = s.max' _

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

source
@[simp]
theorem finset.order_emb_of_fin_singleton {α : Type u_1} [linear_order α] (a : α) (i : fin 1) :
⇑({a}.order_emb_of_fin _) i = a

order_emb_of_fin {a} h sends any argument to a.

source
theorem finset.order_emb_of_fin_unique {α : Type u_1} [linear_order α] {s : finset α} {k : ℕ} (h : s.card = k) {f : fin k → α} (hfs : ∀ (x : fin k), f x ∈ s) (hmono : strict_mono f) :
f = ⇑(s.order_emb_of_fin h)

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

source
theorem finset.order_emb_of_fin_unique' {α : Type u_1} [linear_order α] {s : finset α} {k : ℕ} (h : s.card = k) {f : fin k ↪o α} (hfs : ∀ (x : fin k), ⇑f x ∈ s) :
f = s.order_emb_of_fin h

An order embedding f from fin k to a finset of cardinality k has to coincide with the increasing bijection order_emb_of_fin s h.

source
@[simp]
theorem finset.order_emb_of_fin_eq_order_emb_of_fin_iff {α : Type u_1} [linear_order α] {k l : ℕ} {s : finset α} {i : fin k} {j : fin l} {h : s.card = k} {h' : s.card = l} :
⇑(s.order_emb_of_fin h) i = ⇑(s.order_emb_of_fin h') j ↔ ↑i = ↑j

Two parametrizations order_emb_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 : ℕ) = (j : ℕ).

source
def finset.order_emb_of_card_le {α : Type u_1} [linear_order α] (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 order_emb_of_card_le 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
source
theorem finset.order_emb_of_card_le_mem {α : Type u_1} [linear_order α] (s : finset α) {k : ℕ} (h : k ≤ s.card) (a : fin k) :
⇑(s.order_emb_of_card_le h) a ∈ s
source
@[protected, instance]
meta def finset.has_repr {α : Type u_1} [has_repr α] :
has_repr (finset α)