addBottom_nth_snd — Mathlib

English

The second projection of the nth element of addBottom L equals the nth element of L.

Русский

Второе проекция n-го элемента addBottom L равно n-му элементу L.

LaTeX

$$$ ((\mathrm{addBottom} \, L).\mathrm{nth} \, n).\mathrm{snd} = L.\mathrm{nth} \, n $$$

Lean4

theorem addBottom_nth_snd (L : ListBlank (∀ k, Option (Γ k))) (n : ℕ) : ((addBottom L).nth n).2 = L.nth n := by
  conv => rhs; rw [← addBottom_map L, ListBlank.nth_map]

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