evalFrom_nil

Mathlib.Computability.EpsilonNFA

URI: https://scilib.ai/kg/mathlib#εNFA.evalFrom_nil

English

Evaluating with an empty list yields the ε-closure of the start set.

Русский

Оценка списком, равным пустому, даёт ε-замыкание стартового множества.

LaTeX

$$M.\\evalFrom S [] = M.\\varepsilonClosure S$$

Lean4

@[simp]
theorem evalFrom_nil (S : Set σ) : M.evalFrom S [] = M.εClosure S :=
  rfl

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

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

Разделы

Аффилиация

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