Isomorphism between fin (length l)
and {x // x ∈ l}
#
Given a list `l,
-
if
l
has no duplicates, thenlist.nodup.nth_le_equiv
is the bijection betweenfin (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.(<)
, thenlist.sorted.nth_le_iso
is the same bijection reinterpreted as anorder_iso
.
If l
has no duplicates, then list.nth_le
defines a bijection between fin (length l)
and
the set of elements of l
.
@[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}) :
↑(⇑((list.nodup.nth_le_equiv l H).symm) x) = list.index_of ↑x l
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) :
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
- list.sorted.nth_le_iso l H = {to_equiv := list.nodup.nth_le_equiv l _, map_rel_iff' := _}
@[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}} :
↑(⇑((list.sorted.nth_le_iso l H).symm) x) = list.index_of ↑x l