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) :
α (Fin.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) :
    Fin.take m h v i = v (Fin.castLE h i)
    source
    @[simp]
    theorem Fin.take_zero {n : ℕ} {α : Fin n → Sort u_1} (v : (i : Fin n) → α i) :
    Fin.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) :
    Fin.take 1 ⋯ v = fun (i : Fin 1) => v (Fin.castLE ⋯ i)
    source
    @[simp]
    theorem Fin.take_eq_init {n : ℕ} {α : Fin (n + 1) → Sort u_2} (v : (i : Fin (n + 1)) → α i) :
    Fin.take n ⋯ v = Fin.init v
    source
    @[simp]
    theorem Fin.take_eq_self {n : ℕ} {α : Fin n → Sort u_1} (v : (i : Fin n) → α i) :
    Fin.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) :
    Fin.take m h (Fin.take n' h' v) = Fin.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) :
    Fin.take m h (Fin.init v) = Fin.take m ⋯ v
    source
    theorem Fin.take_repeat {n : ℕ} {α : Type u_2} {n' : ℕ} (m : ℕ) (h : m ≤ n) (a : Fin n' → α) :
    Fin.take (m * n') ⋯ (Fin.repeat n a) = Fin.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) :
    Fin.take m.succ h v = Fin.snoc (Fin.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 : α (Fin.castLE h i)) :
    Fin.take m h (Function.update v (Fin.castLE h i) x) = Function.update (Fin.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) :
    Fin.take m h (Function.update v i x) = Fin.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 (Fin.castAdd n' i)) (v : (i : Fin n') → motive (Fin.natAdd n i)) :
    (Fin.take m ⋯ fun (i : Fin (n + n')) => Fin.addCases u v i) = Fin.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' → α) :
    Fin.take m ⋯ (Fin.append u v) = Fin.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 (Fin.castAdd n' i)) (v : (i : Fin n') → motive (Fin.natAdd n i)) :
    (Fin.take (n + m) ⋯ fun (i : Fin (n + n')) => Fin.addCases u v i) = fun (i : Fin (n + m)) => Fin.addCases u (Fin.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' → α) :
    Fin.take (n + m) ⋯ (Fin.append u v) = Fin.append u (Fin.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 (Fin.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 (Fin.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 = Fin.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 = Fin.take m h v ∘ Fin.cast ⋯

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