evalFrom_cons — Mathlib

English

Consing an element a to the input list corresponds to updating the starting set by a, then continuing with x.

Русский

Добавление элемента a к начальному списку приводит к обновлению стартового множества и продолжению с оставшимся списком.

LaTeX

$$M.evalFrom(S, a :: x) = M.evalFrom(M.stepSet(S,a), x)$$

Lean4

@[simp]
theorem evalFrom_cons (S : Set σ) (a : α) (x : List α) : M.evalFrom S (a :: x) = M.evalFrom (M.stepSet S a) x :=
  rfl

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