vecAlt0_vecAppend — Mathlib

English

Applying vecAlt0 to vecAppend of v with itself recovers v composed with the doubling map.

Русский

Применение vecAlt0 к vecAppend(v,v) восстанавливает v после удвоения индекса.

LaTeX

$$$\\text{vecAlt0}\\mathrm{(}\\mathrm{rfl} ,(\\text{vecAppend} \\mathrm{rfl} \\, v \\, v)\\mathrm{)} = v \\circ (\\lambda n. 2n)$$$

Lean4

theorem vecAlt0_vecAppend (v : Fin n → α) : vecAlt0 rfl (vecAppend rfl v v) = v ∘ (fun n ↦ n + n) :=
  by
  ext i
  simp_rw [Function.comp, vecAlt0, vecAppend_eq_ite]
  split_ifs with h <;> congr
  · rw [Fin.val_mk] at h
    exact (Nat.mod_eq_of_lt h).symm
  · rw [Fin.val_mk, not_lt] at h
    simp only [Nat.mod_eq_sub_mod h]
    refine (Nat.mod_eq_of_lt ?_).symm
    cutsat

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