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} 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.SortedLT.getIso is the same bijection reinterpreted as an OrderIso.

def List.Nodup.getBijectionOfForallMemList {α : Type u_1} (l : List α) (nd : l.Nodup) (h : ∀ (x : α), x ∈ l) : { f : Fin l.length → α // Function.Bijective 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.

@[simp]

theorem List.Nodup.getBijectionOfForallMemList_coe {α : Type u_1} (l : List α) (nd : l.Nodup) (h : ∀ (x : α), x ∈ l) (i : Fin l.length) : ↑(getBijectionOfForallMemList l nd h) i = l.get i

def List.Nodup.getEquiv {α : Type u_1} [DecidableEq α] (l : List α) (H : l.Nodup) : Fin l.length ≃ { 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.

@[simp]

theorem List.Nodup.getEquiv_symm_apply_val {α : Type u_1} [DecidableEq α] (l : List α) (H : l.Nodup) (x : { x : α // x ∈ l }) : ↑((getEquiv l H).symm x) = idxOf (↑x) l

@[simp]

theorem List.Nodup.getEquiv_apply_coe {α : Type u_1} [DecidableEq α] (l : List α) (H : l.Nodup) (i : Fin l.length) : ↑((getEquiv l H) i) = l.get i

def List.Nodup.getEquivOfForallMemList {α : Type u_1} [DecidableEq α] (l : List α) (nd : l.Nodup) (h : ∀ (x : α), x ∈ l) : Fin l.length ≃ α

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.

@[simp]

theorem List.Nodup.getEquivOfForallMemList_symm_apply_val {α : Type u_1} [DecidableEq α] (l : List α) (nd : l.Nodup) (h : ∀ (x : α), x ∈ l) (a : α) : ↑((getEquivOfForallMemList l nd h).symm a) = idxOf a l

@[simp]

theorem List.Nodup.getEquivOfForallMemList_apply {α : Type u_1} [DecidableEq α] (l : List α) (nd : l.Nodup) (h : ∀ (x : α), x ∈ l) (i : Fin l.length) : (getEquivOfForallMemList l nd h) i = l.get i

def List.getEquivOfForallCountEqOne {α : Type u_1} [DecidableEq α] (l : List α) (h : ∀ (x : α), count x l = 1) : Fin l.length ≃ α

Alternative phrasing of List.Nodup.getEquivOfForallMemList using List.count.

@[simp]

theorem List.getEquivOfForallCountEqOne_symm_apply_val {α : Type u_1} [DecidableEq α] (l : List α) (h : ∀ (x : α), count x l = 1) (a : α) : ↑((l.getEquivOfForallCountEqOne h).symm a) = idxOf a l

@[simp]

theorem List.getEquivOfForallCountEqOne_apply {α : Type u_1} [DecidableEq α] (l : List α) (h : ∀ (x : α), count x l = 1) (i : Fin l.length) : (l.getEquivOfForallCountEqOne h) i = l[↑i]

@[deprecated List.SortedLE.monotone_get (since := "2025-10-11")]

theorem List.Sorted.get_mono {α : Type u_1} {l : List α} [Preorder α] : l.SortedLE → Monotone l.get

Alias of the forward direction of List.sortedLE_iff_monotone_get.

@[deprecated List.SortedLT.strictMono_get (since := "2025-10-11")]

theorem List.Sorted.get_strictMono {α : Type u_1} {l : List α} [Preorder α] : l.SortedLT → StrictMono l.get

Alias of the forward direction of List.sortedLT_iff_strictMono_get.

def List.SortedLT.getIso {α : Type u_1} [Preorder α] [DecidableEq α] (l : List α) (H : l.SortedLT) : Fin l.length ≃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.

@[deprecated List.SortedLT.getIso (since := "2025-10-11")]

def List.Sorted.getIso {α : Type u_1} [Preorder α] [DecidableEq α] (l : List α) (H : l.SortedLT) : Fin l.length ≃o { x : α // x ∈ l }

Alias of List.SortedLT.getIso.

---

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.

@[simp]

theorem List.SortedLT.coe_getIso_apply {α : Type u_1} [Preorder α] {l : List α} [DecidableEq α] (H : l.SortedLT) {i : Fin l.length} : ↑((getIso l H) i) = l.get i

@[simp]

theorem List.SortedLT.coe_getIso_symm_apply {α : Type u_1} [Preorder α] {l : List α} [DecidableEq α] (H : l.SortedLT) {x : { x : α // x ∈ l }} : ↑((getIso l H).symm x) = idxOf (↑x) l

@[deprecated List.SortedLT.coe_getIso_apply (since := "2025-10-11")]

theorem List.Sorted.coe_getIso_apply {α : Type u_1} [Preorder α] {l : List α} [DecidableEq α] (H : l.SortedLT) {i : Fin l.length} : ↑((SortedLT.getIso l H) i) = l.get i

Alias of List.SortedLT.coe_getIso_apply.

@[deprecated List.SortedLT.coe_getIso_symm_apply (since := "2025-10-11")]

theorem List.Sorted.coe_getIso_symm_apply {α : Type u_1} [Preorder α] {l : List α} [DecidableEq α] (H : l.SortedLT) {x : { x : α // x ∈ l }} : ↑((SortedLT.getIso l H).symm x) = idxOf (↑x) l

Alias of List.SortedLT.coe_getIso_symm_apply.

theorem List.sublist_of_orderEmbedding_getElem?_eq {α : Type u_1} {l l' : List α} (f : ℕ ↪o ℕ) (hf : ∀ (ix : ℕ), l[ix]? = l'[f ix]?) : l.Sublist 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'.

theorem List.sublist_iff_exists_orderEmbedding_getElem?_eq {α : Type u_1} {l l' : List α} : l.Sublist l' ↔ ∃ (f : ℕ ↪o ℕ), ∀ (ix : ℕ), l[ix]? = l'[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'.

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

theorem List.duplicate_iff_exists_distinct_get {α : Type u_1} {l : List α} {x : α} : Duplicate x l ↔ ∃ (n : Fin l.length) (m : Fin l.length) (_ : n < m), x = l.get n ∧ x = l.get 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.