# Documentation

Mathlib.Data.List.NodupEquivFin

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

Given a list l,

• if l has no duplicates, then List.Nodup.getEquiv is the equivalence between Fin (length l) and {x // x ∈ l}∈ l} sending i to ⟨get l i, _⟩ with the inverse sending ⟨x, hx⟩ to ⟨indexOf x l, _⟩;

• if l has no duplicates and contains every element of a type α, then List.Nodup.getEquivOfForallMemList defines an equivalence between Fin (length l) and α; if α does not have decidable equality, then there is a bijection List.Nodup.getBijectionOfForallMemList;

• if l is sorted w.r.t. (<), then List.Sorted.getIso is the same bijection reinterpreted as an OrderIso.

@[simp]
theorem List.Nodup.getBijectionOfForallMemList_coe {α : Type u_1} (l : List α) (nd : ) (h : ∀ (x : α), x l) (i : Fin ()) :
↑() i = List.get l i
def List.Nodup.getBijectionOfForallMemList {α : Type u_1} (l : List α) (nd : ) (h : ∀ (x : α), x l) :
{ f // }

If l lists all the elements of α without duplicates, then List.get defines a bijection Fin l.length → α→ α. See List.Nodup.getEquivOfForallMemList for a version giving an equivalence when there is decidable equality.

Equations
@[simp]
theorem List.Nodup.getEquiv_symm_apply_val {α : Type u_1} [inst : ] (l : List α) (H : ) (x : { x // x l }) :
↑(↑() x) = List.indexOf (x) l
@[simp]
theorem List.Nodup.getEquiv_apply_coe {α : Type u_1} [inst : ] (l : List α) (H : ) (i : Fin ()) :
↑(↑() i) = List.get l i
def List.Nodup.getEquiv {α : Type u_1} [inst : ] (l : List α) (H : ) :
Fin () { x // x l }

If l has no duplicates, then List.get defines an equivalence between Fin (length l) and the set of elements of l.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem List.Nodup.getEquivOfForallMemList_symm_apply_val {α : Type u_1} [inst : ] (l : List α) (nd : ) (h : ∀ (x : α), x l) (a : α) :
↑(↑() a) =
@[simp]
theorem List.Nodup.getEquivOfForallMemList_apply {α : Type u_1} [inst : ] (l : List α) (nd : ) (h : ∀ (x : α), x l) (i : Fin ()) :
↑() i = List.get l i
def List.Nodup.getEquivOfForallMemList {α : Type u_1} [inst : ] (l : List α) (nd : ) (h : ∀ (x : α), x l) :
Fin () α

If l lists all the elements of α without duplicates, then List.get defines an equivalence between Fin l.length and α.

See List.Nodup.getBijectionOfForallMemList for a version without decidable equality.

Equations
• One or more equations did not get rendered due to their size.
theorem List.Sorted.get_mono {α : Type u_1} [inst : ] {l : List α} (h : List.Sorted (fun x x_1 => x x_1) l) :
theorem List.Sorted.get_strictMono {α : Type u_1} [inst : ] {l : List α} (h : List.Sorted (fun x x_1 => x < x_1) l) :
def List.Sorted.getIso {α : Type u_1} [inst : ] [inst : ] (l : List α) (H : List.Sorted (fun x x_1 => x < x_1) l) :
Fin () ≃o { x // x l }

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

Equations
@[simp]
theorem List.Sorted.coe_getIso_apply {α : Type u_1} [inst : ] {l : List α} [inst : ] (H : List.Sorted (fun x x_1 => x < x_1) l) {i : Fin ()} :
↑(().toEmbedding i) = List.get l i
@[simp]
theorem List.Sorted.coe_getIso_symm_apply {α : Type u_1} [inst : ] {l : List α} [inst : ] (H : List.Sorted (fun x x_1 => x < x_1) l) {x : { x // x l }} :
↑(().toEmbedding x) = List.indexOf (x) l
theorem List.sublist_of_orderEmbedding_get?_eq {α : Type u_1} {l : List α} {l' : List α} (f : ) (hf : ∀ (ix : ), List.get? l ix = List.get? l' (f.toEmbedding ix)) :

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

theorem List.sublist_iff_exists_orderEmbedding_get?_eq {α : Type u_1} {l : List α} {l' : List α} :
List.Sublist l l' f, ∀ (ix : ), List.get? l ix = List.get? l' (f.toEmbedding 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'.

theorem List.sublist_iff_exists_fin_orderEmbedding_get_eq {α : Type u_1} {l : List α} {l' : List α} :
List.Sublist l l' f, ∀ (ix : Fin ()), List.get l ix = List.get l' (f.toEmbedding 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'.

theorem List.duplicate_iff_exists_distinct_get {α : Type u_1} {l : List α} {x : α} :
n m x, x = List.get l n x = List.get l m

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

theorem List.duplicate_iff_exists_distinct_nthLe {α : Type u_1} {l : List α} {x : α} :
n hn m hm x, x = List.nthLe l n hn x = List.nthLe l 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.