Theorems · Definition · combinatorics

List.Nodup.getEquiv

{α : Type u_1} → [DecidableEq α] → (l : List α) → 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.

Defined in

Mathlib.Data.List.NodupEquivFin

Cited by

2 results in Mathlib

Foundations

Depth 56 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEq