Documentation

Mathlib.Data.List.NodupEquivFin

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

Given a list l,

def List.Nodup.getBijectionOfForallMemList {α : Type u_1} (l : List α) (nd : l.Nodup) (h : ∀ (x : α), x l) :

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
    Instances For
      @[simp]
      theorem List.Nodup.getBijectionOfForallMemList_coe {α : Type u_1} (l : List α) (nd : l.Nodup) (h : ∀ (x : α), x l) (i : Fin l.length) :
      def List.Nodup.getEquiv {α : Type u_1} [DecidableEq α] (l : List α) (H : l.Nodup) :
      Fin l.length { 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
        Instances For
          @[simp]
          theorem List.Nodup.getEquiv_symm_apply_val {α : Type u_1} [DecidableEq α] (l : List α) (H : l.Nodup) (x : { x : α // x l }) :
          ((getEquiv l H).symm x) = idxOf (↑x) l
          @[simp]
          theorem List.Nodup.getEquiv_apply_coe {α : Type u_1} [DecidableEq α] (l : List α) (H : l.Nodup) (i : Fin l.length) :
          ((getEquiv l H) i) = l.get i
          def List.Nodup.getEquivOfForallMemList {α : Type u_1} [DecidableEq α] (l : List α) (nd : l.Nodup) (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
            Instances For
              @[simp]
              theorem List.Nodup.getEquivOfForallMemList_apply {α : Type u_1} [DecidableEq α] (l : List α) (nd : l.Nodup) (h : ∀ (x : α), x l) (i : Fin l.length) :
              @[simp]
              theorem List.Nodup.getEquivOfForallMemList_symm_apply_val {α : Type u_1} [DecidableEq α] (l : List α) (nd : l.Nodup) (h : ∀ (x : α), x l) (a : α) :
              ((getEquivOfForallMemList l nd h).symm a) = idxOf a l
              theorem List.Sorted.get_mono {α : Type u_1} [Preorder α] {l : List α} (h : Sorted (fun (x1 x2 : α) => x1 x2) l) :
              theorem List.Sorted.get_strictMono {α : Type u_1} [Preorder α] {l : List α} (h : Sorted (fun (x1 x2 : α) => x1 < x2) l) :
              def List.Sorted.getIso {α : Type u_1} [Preorder α] [DecidableEq α] (l : List α) (H : Sorted (fun (x1 x2 : α) => x1 < x2) l) :
              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.

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

                  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'.

                  @[deprecated List.sublist_of_orderEmbedding_getElem?_eq (since := "2025-02-15")]
                  theorem List.sublist_of_orderEmbedding_get?_eq {α : Type u_1} {l l' : List α} (f : ↪o ) (hf : ∀ (ix : ), l[ix]? = l'[f ix]?) :
                  l.Sublist l'

                  Alias of List.sublist_of_orderEmbedding_getElem?_eq.


                  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_getElem?_eq {α : Type u_1} {l l' : List α} :
                  l.Sublist l' ∃ (f : ↪o ), ∀ (ix : ), l[ix]? = 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'.

                  @[deprecated List.sublist_iff_exists_orderEmbedding_getElem?_eq (since := "2025-02-15")]
                  theorem List.sublist_iff_exists_orderEmbedding_get?_eq {α : Type u_1} {l l' : List α} :
                  l.Sublist l' ∃ (f : ↪o ), ∀ (ix : ), l[ix]? = l'[f ix]?

                  Alias of List.sublist_iff_exists_orderEmbedding_getElem?_eq.


                  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 l' : List α} :
                  l.Sublist l' ∃ (f : Fin l.length ↪o Fin l'.length), ∀ (ix : Fin l.length), l.get ix = l'.get (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 : α} :
                  Duplicate x l ∃ (n : Fin l.length) (m : Fin l.length) (_ : n < m), x = l.get n x = l.get 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.