eval_append_singleton — Mathlib

English

Appending a singleton [a] to a word x yields stepping from the value of x by a.

Русский

Добавление одиночного слова [a] к списку x эквивалентно переходу по a от значения x.

LaTeX

$$eval_append_singleton (x) (a) : M.eval (x ++ [a]) = M.stepSet (M.eval x) a$$

Lean4

@[simp]
theorem eval_append_singleton (x : List α) (a : α) : M.eval (x ++ [a]) = M.stepSet (M.eval x) a :=
  evalFrom_append_singleton ..

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