Theorems · Definition · combinatorics

List.SortedLT.getIso

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

Defined in

Mathlib.Data.List.NodupEquivFin

Cited by

2 results in Mathlib

Foundations

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

Assumes

PreorderDecidableEq