eval_reindex — Mathlib

English

Evaluating a reindexed DFA on a word x yields applying g to the evaluation of the original on x.

Русский

Оценка переиндексированного DFA на слово x даёт применение g к оценке исходного на то же самое слово x.

LaTeX

$$$ (\\mathrm{reindex} g M).\\mathrm{eval} x = g (M.\\mathrm{eval} x) $$$

Lean4

@[simp]
theorem eval_reindex (g : σ ≃ σ') (x : List α) : (reindex g M).eval x = g (M.eval x) := by simp [eval]

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