step_toDFA — Mathlib

English

In the DFA constructed from L, the transition on input a from a state s corresponds to taking the left quotient by a appended to the representative word: the next state's value is s.val.leftQuotient [a].

Русский

Переход по символу a из состояния s в ДКА соответствует левому делителю с добавлением a к представителю слова: следующее состояние имеет значение s.val.leftQuotient [a].

LaTeX

$$$(L.toDFA.step\; s\; a).val = s.val.leftQuotient [a].$$$

Lean4

@[simp]
theorem step_toDFA (s : Set.range L.leftQuotient) (a : α) : (L.toDFA.step s a).val = s.val.leftQuotient [a] :=
  rfl

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