addBottom_modifyNth — Mathlib

English

Applying modifyNth under addBottom corresponds to modifying the Nth element of the base list inside addBottom.

Русский

Применение modifyNth к addBottom эквивалентно изменению N-го элемента базового списка внутри addBottom.

LaTeX

$$$ (\mathrm{addBottom} \, L).\mathrm{modifyNth} (\lambda a, f a.2) \, n = \mathrm{addBottom} (L.\mathrm{modifyNth} f \, n) $$$

Lean4

theorem addBottom_modifyNth (f : (∀ k, Option (Γ k)) → ∀ k, Option (Γ k)) (L : ListBlank (∀ k, Option (Γ k))) (n : ℕ) :
    (addBottom L).modifyNth (fun a ↦ (a.1, f a.2)) n = addBottom (L.modifyNth f n) :=
  by
  cases n <;> simp only [addBottom, ListBlank.head_cons, ListBlank.modifyNth, ListBlank.tail_cons]
  congr; symm; apply ListBlank.map_modifyNth; intro; rfl

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