toDFA_correct — Mathlib

English

The NFA obtained via the subset construction from a DFA accepts exactly the same words as the original DFA.

Русский

Автомат, полученный методом подмножества из данного ДКА, принимает ровно те же слова, что и исходный ДКА.

LaTeX

$$$M.toDFA.accepts = M.accepts$$$

Lean4

@[simp]
theorem toDFA_correct : M.toDFA.accepts = M.accepts := by
  ext x
  rw [mem_accepts, DFA.mem_accepts]
  constructor <;> · exact fun ⟨w, h2, h3⟩ => ⟨w, h3, h2⟩

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