eval_comap

Mathlib.Computability.DFA

URI: https://scilib.ai/kg/mathlib#DFA.eval_comap

English

A simp-lemma for evalFrom under comap: the same as above, expressed for a simp attribute.

Русский

Упрощённая лемма для evalFrom под comap: то же самое выражено через simp-атрибут.

LaTeX

$$$ @[simp] \; \text{theorem} \; M.{\mathrm{evalFrom}}(s, x) = M.{\mathrm{evalFrom}}(s, x.map f) $$$

Lean4

@[simp]
theorem eval_comap (f : α' → α) (x : List α') : (M.comap f).eval x = M.eval (x.map f) := by simp [eval]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru