Documentation

Mathlib.Data.List.NodupEquivFin

Equivalence between Fin (length l) and elements of a list #

Given a list l,

@[simp]
theorem List.Nodup.getBijectionOfForallMemList_coe {α : Type u_1} (l : List α) (nd : List.Nodup l) (h : ∀ (x : α), x l) (i : Fin (List.length l)) :
def List.Nodup.getBijectionOfForallMemList {α : Type u_1} (l : List α) (nd : List.Nodup l) (h : ∀ (x : α), x l) :
{ f : Fin (List.length l)α // Function.Bijective f }

If l lists all the elements of α without duplicates, then List.get defines a bijection Fin l.length → α. See List.Nodup.getEquivOfForallMemList for a version giving an equivalence when there is decidable equality.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem List.Nodup.getEquiv_symm_apply_val {α : Type u_1} [DecidableEq α] (l : List α) (H : List.Nodup l) (x : { x : α // x l }) :
    ((List.Nodup.getEquiv l H).symm x) = List.indexOf (x) l
    @[simp]
    theorem List.Nodup.getEquiv_apply_coe {α : Type u_1} [DecidableEq α] (l : List α) (H : List.Nodup l) (i : Fin (List.length l)) :
    ((List.Nodup.getEquiv l H) i) = List.get l i
    def List.Nodup.getEquiv {α : Type u_1} [DecidableEq α] (l : List α) (H : List.Nodup l) :
    Fin (List.length l) { 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.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem List.Nodup.getEquivOfForallMemList_symm_apply_val {α : Type u_1} [DecidableEq α] (l : List α) (nd : List.Nodup l) (h : ∀ (x : α), x l) (a : α) :
      @[simp]
      theorem List.Nodup.getEquivOfForallMemList_apply {α : Type u_1} [DecidableEq α] (l : List α) (nd : List.Nodup l) (h : ∀ (x : α), x l) (i : Fin (List.length l)) :
      def List.Nodup.getEquivOfForallMemList {α : Type u_1} [DecidableEq α] (l : List α) (nd : List.Nodup l) (h : ∀ (x : α), x l) :

      If l lists all the elements of α without duplicates, then List.get defines an equivalence between Fin l.length and α.

      See List.Nodup.getBijectionOfForallMemList for a version without decidable equality.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem List.Sorted.get_mono {α : Type u_1} [Preorder α] {l : List α} (h : List.Sorted (fun (x x_1 : α) => x x_1) l) :
        theorem List.Sorted.get_strictMono {α : Type u_1} [Preorder α] {l : List α} (h : List.Sorted (fun (x x_1 : α) => x < x_1) l) :
        def List.Sorted.getIso {α : Type u_1} [Preorder α] [DecidableEq α] (l : List α) (H : List.Sorted (fun (x x_1 : α) => x < x_1) l) :
        Fin (List.length l) ≃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.

        Equations
        Instances For
          @[simp]
          theorem List.Sorted.coe_getIso_apply {α : Type u_1} [Preorder α] {l : List α} [DecidableEq α] (H : List.Sorted (fun (x x_1 : α) => x < x_1) l) {i : Fin (List.length l)} :
          ((List.Sorted.getIso l H) i) = List.get l i
          @[simp]
          theorem List.Sorted.coe_getIso_symm_apply {α : Type u_1} [Preorder α] {l : List α} [DecidableEq α] (H : List.Sorted (fun (x x_1 : α) => x < x_1) l) {x : { x : α // x l }} :
          theorem List.sublist_of_orderEmbedding_get?_eq {α : Type u_1} {l : List α} {l' : List α} (f : ↪o ) (hf : ∀ (ix : ), List.get? l ix = List.get? l' (f ix)) :

          If there is f, an order-preserving embedding of into such that any element of l found at index ix can be found at index f ix in l', then Sublist l l'.

          theorem List.sublist_iff_exists_orderEmbedding_get?_eq {α : Type u_1} {l : List α} {l' : List α} :
          List.Sublist l l' ∃ (f : ↪o ), ∀ (ix : ), List.get? l ix = List.get? l' (f ix)

          A l : List α is Sublist l l' for l' : List α iff there is f, an order-preserving embedding of into such that any element of l found at index ix can be found at index f ix in l'.

          theorem List.sublist_iff_exists_fin_orderEmbedding_get_eq {α : Type u_1} {l : List α} {l' : List α} :
          List.Sublist l l' ∃ (f : Fin (List.length l) ↪o Fin (List.length l')), ∀ (ix : Fin (List.length l)), List.get l ix = List.get l' (f ix)

          A l : List α is Sublist l l' for l' : List α iff there is f, an order-preserving embedding of Fin l.length into Fin l'.length such that any element of l found at index ix can be found at index f ix in l'.

          theorem List.duplicate_iff_exists_distinct_get {α : Type u_1} {l : List α} {x : α} :
          List.Duplicate x l ∃ (n : Fin (List.length l)) (m : Fin (List.length l)) (_ : n < m), x = List.get l n x = List.get l m

          An element x : α of l : List α is a duplicate iff it can be found at two distinct indices n m : ℕ inside the list l.

          @[deprecated List.duplicate_iff_exists_distinct_get]
          theorem List.duplicate_iff_exists_distinct_nthLe {α : Type u_1} {l : List α} {x : α} :
          List.Duplicate x l ∃ (n : ) (hn : n < List.length l) (m : ) (hm : m < List.length l) (_ : n < m), x = List.nthLe l n hn x = List.nthLe l m hm

          An element x : α of l : List α is a duplicate iff it can be found at two distinct indices n m : ℕ inside the list l.