toεNFA_εClosure — Mathlib

English

For any εNFA M, evaluating from a set S in M corresponds to evaluating from S after converting to an εNFA; i.e., the evaluation respects the ε-closure when moving to the εNFA form.

Русский

Для εNFA M вычисления от множества S сохраняются при переходе к форме εNFA; то есть вычисление совместимо с ε-замыканием.

LaTeX

$$$M.toNFA.\\varepsilonClosure S = S \\Rightarrow M.toεNFA.\\varepsilonClosure S = S$$$

Lean4

@[simp]
theorem toεNFA_εClosure (M : NFA α σ) (S : Set σ) : M.toεNFA.εClosure S = S :=
  by
  ext a
  refine ⟨?_, εNFA.εClosure.base _⟩
  rintro (⟨_, h⟩ | ⟨_, _, h, _⟩)
  · exact h
  · cases h

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