English
For any function f : α' → α, the evaluation from s on a mapped word equals the evaluation from s on the word mapped by f: (M.comap f).evalFrom s x = M.evalFrom s (x.map f).
Русский
Для любой функции f: α' → α вычисление из начала s на слово, отображённое по f, равно вычислению из начала s на слово, отображённое через f: (M.comap f).evalFrom s x = M.evalFrom s (x.map f).
LaTeX
$$$ (M.{\mathrm{comap}}\, f).\mathrm{evalFrom}(s, x) = M.\mathrm{evalFrom}(s, x.map f) $$$
Lean4
@[simp]
theorem evalFrom_comap (f : α' → α) (s : σ) (x : List α') : (M.comap f).evalFrom s x = M.evalFrom s (x.map f) := by
induction x using List.reverseRecOn with
| nil => simp
| append_singleton x a ih => simp [ih]
