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 an 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 α.