ofFn_take_eq_take_ofFn — Mathlib

English

List.ofFn (Fin.take m h v) equals List.take m (List.ofFn v).

Русский

List.ofFn (Fin.take m h v) равно List.take m (List.ofFn v).

LaTeX

$$$\\operatorname{List.ofFn}(\\operatorname{Fin.take}(m,h,v)) = \\operatorname{List.take}(m)(\\operatorname{List.ofFn}v)$$$

Lean4

/-- `Fin.take` intertwines with `List.take` via `List.ofFn`. -/
theorem ofFn_take_eq_take_ofFn {α : Type*} {m : ℕ} (h : m ≤ n) (v : Fin n → α) :
    List.ofFn (take m h v) = (List.ofFn v).take m :=
  List.ext_get (by simp [h]) (fun n h1 h2 => by simp)

Похожие утверждения