Equivalence between `fin (length l)` and elements of a list #

Given a list l,

if l has no duplicates, then list.nodup.nth_le_equiv is the equivalence between fin (length l) and {x // x ∈ l} sending ⟨i, hi⟩ to ⟨nth_le l i hi, _⟩ with the inverse sending ⟨x, hx⟩ to ⟨index_of x l, _⟩;
if l has no duplicates and contains every element of a type α, then list.nodup.nth_le_equiv_of_forall_mem_list defines an equivalence between fin (length l) and α; if α does not have decidable equality, then there is a bijection list.nodup.nth_le_bijection_of_forall_mem_list;
if l is sorted w.r.t. (<), then list.sorted.nth_le_iso is the same bijection reinterpreted as an order_iso.

@[simp]

theorem list.nodup.nth_le_bijection_of_forall_mem_list_coe {α : Type u_1} (l : list α) (nd : l.nodup) (h : ∀ (x : α), x ∈ l) (i : fin l.length) :

↑(list.nodup.nth_le_bijection_of_forall_mem_list l nd h) i = l.nth_le ↑i _

source

def list.nodup.nth_le_bijection_of_forall_mem_list {α : Type u_1} (l : list α) (nd : l.nodup) (h : ∀ (x : α), x ∈ l) :

{f // function.bijective f}

If l lists all the elements of α without duplicates, then list.nth_le defines a bijection fin l.length → α. See list.nodup.nth_le_equiv_of_forall_mem_list for a version giving an equivalence when there is decidable equality.

Equations

list.nodup.nth_le_bijection_of_forall_mem_list l nd h = ⟨λ (i : fin l.length), l.nth_le ↑i _, _⟩

source

@[simp]

theorem list.nodup.nth_le_equiv_apply_coe {α : Type u_1} [decidable_eq α] (l : list α) (H : l.nodup) (i : fin l.length) :

↑(⇑(list.nodup.nth_le_equiv l H) i) = l.nth_le ↑i _

source

def list.nodup.nth_le_equiv {α : Type u_1} [decidable_eq α] (l : list α) (H : l.nodup) :

fin l.length ≃ {x // x ∈ l}

If l has no duplicates, then list.nth_le defines an equivalence between fin (length l) and the set of elements of l.

Equations

list.nodup.nth_le_equiv l H = {to_fun := λ (i : fin l.length), ⟨l.nth_le ↑i _, _⟩, inv_fun := λ (x : {x // x ∈ l}), ⟨list.index_of ↑x l, _⟩, left_inv := _, right_inv := _}

source

@[simp]

theorem list.nodup.nth_le_equiv_symm_apply_coe {α : Type u_1} [decidable_eq α] (l : list α) (H : l.nodup) (x : {x // x ∈ l}) :

↑(⇑((list.nodup.nth_le_equiv l H).symm) x) = list.index_of ↑x l

source

@[simp]

theorem list.nodup.nth_le_equiv_of_forall_mem_list_symm_apply_coe {α : Type u_1} [decidable_eq α] (l : list α) (nd : l.nodup) (h : ∀ (x : α), x ∈ l) (a : α) :

↑(⇑((list.nodup.nth_le_equiv_of_forall_mem_list l nd h).symm) a) = list.index_of a l

source

@[simp]

theorem list.nodup.nth_le_equiv_of_forall_mem_list_apply {α : Type u_1} [decidable_eq α] (l : list α) (nd : l.nodup) (h : ∀ (x : α), x ∈ l) (i : fin l.length) :

⇑(list.nodup.nth_le_equiv_of_forall_mem_list l nd h) i = l.nth_le ↑i _

source

def list.nodup.nth_le_equiv_of_forall_mem_list {α : Type u_1} [decidable_eq α] (l : list α) (nd : l.nodup) (h : ∀ (x : α), x ∈ l) :

fin l.length ≃ α

If l lists all the elements of α without duplicates, then list.nth_le defines an equivalence between fin l.length and α.

See list.nodup.nth_le_bijection_of_forall_mem_list for a version without decidable equality.

Equations

list.nodup.nth_le_equiv_of_forall_mem_list l nd h = {to_fun := λ (i : fin l.length), l.nth_le ↑i _, inv_fun := λ (a : α), ⟨list.index_of a l, _⟩, left_inv := _, right_inv := _}

source

theorem list.sorted.nth_le_mono {α : Type u_1} [preorder α] {l : list α} (h : list.sorted has_le.le l) :

monotone (λ (i : fin l.length), l.nth_le ↑i _)

source

theorem list.sorted.nth_le_strict_mono {α : Type u_1} [preorder α] {l : list α} (h : list.sorted has_lt.lt l) :

strict_mono (λ (i : fin l.length), l.nth_le ↑i _)

source

def list.sorted.nth_le_iso {α : Type u_1} [preorder α] [decidable_eq α] (l : list α) (H : list.sorted has_lt.lt l) :

fin l.length ≃o {x // x ∈ l}

If l is a list sorted w.r.t. (<), then list.nth_le defines an order isomorphism between fin (length l) and the set of elements of l.

Equations

list.sorted.nth_le_iso l H = {to_equiv := list.nodup.nth_le_equiv l _, map_rel_iff' := _}

source

@[simp]

theorem list.sorted.coe_nth_le_iso_apply {α : Type u_1} [preorder α] {l : list α} [decidable_eq α] (H : list.sorted has_lt.lt l) {i : fin l.length} :

↑(⇑(list.sorted.nth_le_iso l H) i) = l.nth_le ↑i _

source

@[simp]

theorem list.sorted.coe_nth_le_iso_symm_apply {α : Type u_1} [preorder α] {l : list α} [decidable_eq α] (H : list.sorted has_lt.lt l) {x : {x // x ∈ l}} :

↑(⇑((list.sorted.nth_le_iso l H).symm) x) = list.index_of ↑x l

source

theorem list.sublist_of_order_embedding_nth_eq {α : Type u_1} {l l' : list α} (f : ℕ ↪o ℕ) (hf : ∀ (ix : ℕ), l.nth ix = l'.nth (⇑f ix)) :

l <+ l'

If there is f, an order-preserving embedding of ℕ into ℕ such that any element of l found at index ix can be found at index f ix in l', then sublist l l'.

source

theorem list.sublist_iff_exists_order_embedding_nth_eq {α : Type u_1} {l l' : list α} :

l <+ l' ↔ ∃ (f : ℕ ↪o ℕ), ∀ (ix : ℕ), l.nth ix = l'.nth (⇑f ix)

A l : list α is sublist l l' for l' : list α iff there is f, an order-preserving embedding of ℕ into ℕ such that any element of l found at index ix can be found at index f ix in l'.

source

theorem list.sublist_iff_exists_fin_order_embedding_nth_le_eq {α : Type u_1} {l l' : list α} :

l <+ l' ↔ ∃ (f : fin l.length ↪o fin l'.length), ∀ (ix : fin l.length), l.nth_le ↑ix _ = l'.nth_le ↑(⇑f ix) _

A l : list α is sublist l l' for l' : list α iff there is f, an order-preserving embedding of fin l.length into fin l'.length such that any element of l found at index ix can be found at index f ix in l'.

source

theorem list.duplicate_iff_exists_distinct_nth_le {α : Type u_1} {l : list α} {x : α} :

list.duplicate x l ↔ ∃ (n : ℕ) (hn : n < l.length) (m : ℕ) (hm : m < l.length) (h : n < m), x = l.nth_le n hn ∧ x = l.nth_le m hm

An element x : α of l : list α is a duplicate iff it can be found at two distinct indices n m : ℕ inside the list l.

Equivalence between fin (length l) and elements of a list #

Equivalence between `fin (length l)` and elements of a list #