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
πŸ”Έ coverage
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.

Instances For
    source
    πŸ“ coverage
    @[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
    πŸ“ coverage
    @[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
    πŸ“ coverage
    @[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
    πŸ“ coverage
    @[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
    πŸ“ coverage
    @[simp]
    theorem Fin.take_eq_self {n : β„•} {Ξ± : Fin n β†’ Sort u_1} (v : (i : Fin n) β†’ Ξ± i) :
    take n β‹― v = v
    source
    πŸ“ coverage
    @[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
    πŸ“ coverage
    @[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
    πŸ“ coverage
    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
    πŸ“ coverage
    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
    πŸ“ coverage
    @[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
    πŸ“ coverage
    @[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
    πŸ“ coverage
    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
    πŸ“ coverage
    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
    πŸ“ coverage
    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
    πŸ“ coverage
    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
    πŸ“ coverage
    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
    πŸ“ coverage
    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
    πŸ“ coverage
    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
    πŸ“ coverage
    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 Ξ±.