English
Mapping a function f over a ListBlank L, the nth element equals f applied to the nth element of L: (l.map f).nth n = f(l.nth n).
Русский
Отображение функции над ListBlank L сохраняет формулу: (l.map f).nth n = f(l.nth n).
LaTeX
$$$\forall {\Gamma \Gamma'} [Inhabited(\Gamma)] [Inhabited(\Gamma')] (f : PointedMap(\Gamma, \Gamma')) (l : ListBlank(\Gamma)) (n : \mathbb{N}): (l.map f).nth n = f(l.nth n)$$$
Lean4
@[simp]
theorem nth_map {Γ Γ'} [Inhabited Γ] [Inhabited Γ'] (f : PointedMap Γ Γ') (l : ListBlank Γ) (n : ℕ) :
(l.map f).nth n = f (l.nth n) := by
refine l.induction_on fun l ↦ ?_
simp only [ListBlank.map_mk, ListBlank.nth_mk, ← List.getD_default_eq_getI]
rw [← List.getD_map _ _ f]
simp
