Documentation

Mathlib.Data.Fin.Tuple.Take

Take operations on tuples #

We define the take operation on n-tuples, which restricts a tuple to its first m elements.

source
def Fin.take {n : ℕ} {α : Fin n → Sort u_1} (m : ℕ) (h : m ≤ n) (v : (i : Fin n) → α i) (i : Fin m) :
α (castLE h i)

Take the first m elements of an n-tuple where m ≤ n, returning an m-tuple.

Equations
    Instances For
      source
      @[simp]
      theorem Fin.take_apply {n : ℕ} {α : Fin n → Sort u_1} (m : ℕ) (h : m ≤ n) (v : (i : Fin n) → α i) (i : Fin m) :
      take m h v i = v (castLE h i)
      source
      @[simp]
      theorem Fin.take_zero {n : ℕ} {α : Fin n → Sort u_1} (v : (i : Fin n) → α i) :
      take 0 ⋯ v = fun (i : Fin 0) => i.elim0
      source
      @[simp]
      theorem Fin.take_one {n : ℕ} {α : Fin (n + 1) → Sort u_2} (v : (i : Fin (n + 1)) → α i) :
      take 1 ⋯ v = fun (i : Fin 1) => v (castLE ⋯ i)
      source
      @[simp]
      theorem Fin.take_eq_init {n : ℕ} {α : Fin (n + 1) → Sort u_2} (v : (i : Fin (n + 1)) → α i) :
      take n ⋯ v = init v
      source
      @[simp]
      theorem Fin.take_eq_self {n : ℕ} {α : Fin n → Sort u_1} (v : (i : Fin n) → α i) :
      take n ⋯ v = v
      source
      @[simp]
      theorem Fin.take_take {n : ℕ} {α : Fin n → Sort u_1} {m n' : ℕ} (h : m ≤ n') (h' : n' ≤ n) (v : (i : Fin n) → α i) :
      take m h (take n' h' v) = take m ⋯ v
      source
      @[simp]
      theorem Fin.take_init {n : ℕ} {α : Fin (n + 1) → Sort u_2} (m : ℕ) (h : m ≤ n) (v : (i : Fin (n + 1)) → α i) :
      take m h (init v) = take m ⋯ v
      source
      theorem Fin.take_repeat {n : ℕ} {α : Type u_2} {n' : ℕ} (m : ℕ) (h : m ≤ n) (a : Fin n' → α) :
      take (m * n') ⋯ («repeat» n a) = «repeat» m a
      source
      theorem Fin.take_succ_eq_snoc {n : ℕ} {α : Fin n → Sort u_1} (m : ℕ) (h : m < n) (v : (i : Fin n) → α i) :
      take m.succ h v = snoc (take m ⋯ v) (v ⟨m, h⟩)

      Taking m + 1 elements is equal to taking m elements and adding the (m + 1)th one.

      source
      @[simp]
      theorem Fin.take_update_of_lt {n : ℕ} {α : Fin n → Sort u_1} (m : ℕ) (h : m ≤ n) (v : (i : Fin n) → α i) (i : Fin m) (x : α (castLE h i)) :
      take m h (Function.update v (castLE h i) x) = Function.update (take m h v) i x

      take commutes with update for indices in the range of take.

      source
      @[simp]
      theorem Fin.take_update_of_ge {n : ℕ} {α : Fin n → Sort u_1} (m : ℕ) (h : m ≤ n) (v : (i : Fin n) → α i) (i : Fin n) (hi : ↑i ≥ m) (x : α i) :
      take m h (Function.update v i x) = take m h v

      take is the same after update for indices outside the range of take.

      source
      theorem Fin.take_addCases_left {n n' : ℕ} {motive : Fin (n + n') → Sort u_2} (m : ℕ) (h : m ≤ n) (u : (i : Fin n) → motive (castAdd n' i)) (v : (i : Fin n') → motive (natAdd n i)) :
      (take m ⋯ fun (i : Fin (n + n')) => addCases u v i) = take m h u

      Taking the first m ≤ n elements of an addCases u v, where u is a n-tuple, is the same as taking the first m elements of u.

      source
      theorem Fin.take_append_left {n n' : ℕ} {α : Sort u_2} (m : ℕ) (h : m ≤ n) (u : Fin n → α) (v : Fin n' → α) :
      take m ⋯ (append u v) = take m h u

      Version of take_addCases_left that specializes addCases to append.

      source
      theorem Fin.take_addCases_right {n n' : ℕ} {motive : Fin (n + n') → Sort u_2} (m : ℕ) (h : m ≤ n') (u : (i : Fin n) → motive (castAdd n' i)) (v : (i : Fin n') → motive (natAdd n i)) :
      (take (n + m) ⋯ fun (i : Fin (n + n')) => addCases u v i) = fun (i : Fin (n + m)) => addCases u (take m h v) i

      Taking the first n + m elements of an addCases u v, where v is a n'-tuple and m ≤ n', is the same as appending u with the first m elements of v.

      source
      theorem Fin.take_append_right {n n' : ℕ} {α : Sort u_2} (m : ℕ) (h : m ≤ n') (u : Fin n → α) (v : Fin n' → α) :
      take (n + m) ⋯ (append u v) = append u (take m h v)

      Version of take_addCases_right that specializes addCases to append.

      source
      theorem Fin.ofFn_take_eq_take_ofFn {n : ℕ} {α : Type u_2} {m : ℕ} (h : m ≤ n) (v : Fin n → α) :
      List.ofFn (take m h v) = List.take m (List.ofFn v)

      Fin.take intertwines with List.take via List.ofFn.

      source
      theorem Fin.ofFn_take_get {α : Type u_2} {m : ℕ} (l : List α) (h : m ≤ l.length) :
      List.ofFn (take m h l.get) = List.take m l

      Alternative version of take_eq_take_list_ofFn with l : List α instead of v : Fin n → α.

      source
      theorem Fin.get_take_eq_take_get_comp_cast {α : Type u_2} {m : ℕ} (l : List α) (h : m ≤ l.length) :
      (List.take m l).get = take m h l.get ∘ Fin.cast ⋯

      Fin.take intertwines with List.take via List.get.

      source
      theorem Fin.get_take_ofFn_eq_take_comp_cast {n : ℕ} {α : Type u_2} {m : ℕ} (v : Fin n → α) (h : m ≤ n) :
      (List.take m (List.ofFn v)).get = take m h v ∘ Fin.cast ⋯

      Alternative version of take_eq_take_list_get with v : Fin n → α instead of l : List α.