Take operations on tuples

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

• Fin.take: Given h : m ≤ n, Fin.take m h v for a n-tuple v = (v 0, ..., v (n - 1)) is the m-tuple (v 0, ..., v (m - 1)).

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

• Fin.take m h v i = v (Fin.castLE h i)

@[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)

@[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

@[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)

@[simp]

theorem Fin.take_eq_init {n : ℕ} {α : Fin (n + 1) → Sort u_2} (v : (i : Fin (n + 1)) → α i) : take n ⋯ v = init v

@[simp]

theorem Fin.take_eq_self {n : ℕ} {α : Fin n → Sort u_1} (v : (i : Fin n) → α i) : take n ⋯ v = v

@[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

@[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

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

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.

@[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.

@[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.

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.

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.

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.

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.

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.

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

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.

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