evalFrom_empty — Mathlib

English

Given S and empty list, evalFrom equals ε-closure of S (reiterated).

Русский

Для любого S и пустого списка evalFrom равняется ε-замыканию S.

LaTeX

$$EvalFrom_nil_placeholder$$

Lean4

@[simp]
theorem evalFrom_empty (x : List α) : M.evalFrom ∅ x = ∅ := by
  induction x using List.reverseRecOn with
  | nil => rw [evalFrom_nil, εClosure_empty]
  | append_singleton x a ih => rw [evalFrom_append_singleton, ih, stepSet_empty]

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