x ∈ l}` #

Given a list `l,

if l has no duplicates, then list.nodup.nth_le_equiv is the bijection between fin (length l) and {x // x ∈ l} sending ⟨i, hi⟩ to ⟨nth_le l i hi, _⟩ with the inverse sending ⟨x, hx⟩ to ⟨index_of x l, _⟩;
if l is sorted w.r.t. (<), then list.sorted.nth_le_iso is the same bijection reinterpreted as an order_iso.

def list.nodup.nth_le_equiv {α : Type u_1} [decidable_eq α] (l : list α) (H : l.nodup) :

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) :

theorem list.sorted.nth_le_strict_mono {α : Type u_1} [preorder α] {l : list α} (h : list.sorted has_lt.lt l) :

def list.sorted.nth_le_iso {α : Type u_1} [preorder α] [decidable_eq α] (l : list α) (H : list.sorted has_lt.lt 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}} :

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