English
For any F: Γ → Γ', f: Γ → Γ with H: ∀ x, F(f x) = f'(F x), we have (L.modifyNth f n).map F = (L.map F).modifyNth f' n.
Русский
Для отображений F: Γ → Γ', f: Γ → Γ и условия H: ∀ x, F(f x) = f'(F x) выполняется: (L.modifyNth f n).map F = (L.map F).modifyNth f' n.
LaTeX
$$$\forall {\Gamma \Gamma'} [Inhabited(\Gamma)] [Inhabited(\Gamma')] (F : PointedMap(\Gamma, \Gamma')) (f : \Gamma → \Gamma) (f' : \Gamma' → \Gamma') (H : \forall x, F(f x) = f'(F x)) (n) (L : ListBlank(\Gamma)),\ (L.modifyNth f n).map F = (L.map F).modifyNth f' n$$$
Lean4
theorem map_modifyNth {Γ Γ'} [Inhabited Γ] [Inhabited Γ'] (F : PointedMap Γ Γ') (f : Γ → Γ) (f' : Γ' → Γ')
(H : ∀ x, F (f x) = f' (F x)) (n) (L : ListBlank Γ) : (L.modifyNth f n).map F = (L.map F).modifyNth f' n := by
induction n generalizing L <;>
simp only [*, ListBlank.head_map, ListBlank.modifyNth, ListBlank.map_cons, ListBlank.tail_map]
