mem_accept_toDFA — Mathlib

English

For a state s of the DFA built from L, s is accepting if and only if the empty word lies in the left quotient represented by s.

Русский

Состояние s построенного ДКА является принимающим тогда и только тогда, когда пустое слово принадлежит левому делителю, представляемому этим состоянием.

LaTeX

$$$s \in L.toDFA.accept \iff [] \in s.val$$$

Lean4

@[simp]
theorem mem_accept_toDFA (s : Set.range L.leftQuotient) : s ∈ L.toDFA.accept ↔ [] ∈ s.val :=
  Iff.rfl

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