mathlib documentation

data.list.nodup_equiv_fin

Isomorphism between fin (length l) and {x // x ∈ l} #

Given a list `l,

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 a bijection between fin (length l) and the set of elements of l.

Equations
@[simp]
theorem list.nodup.coe_nth_le_equiv_apply {α : Type u_1} [decidable_eq α] {l : list α} (H : l.nodup) (i : fin l.length) :
@[simp]
theorem list.nodup.coe_nth_le_equiv_symm_apply {α : Type u_1} [decidable_eq α] {l : list α} (H : l.nodup) (x : {x // x l}) :
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 _)
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 _)
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
@[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} :
@[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}} :