English
A language is regular if and only if it is defined by a DFA with finite states.
Русский
Язык регулярен тогда и только тогда, когда его определяет DFA с конечным числом состояний.
LaTeX
$$$ L.IsRegular \iff \exists \sigma : Type v, \exists _ : Fintype \sigma, \exists M : DFA T \sigma, M.accepts = L $$$
Lean4
/-- A language is regular if and only if it is defined by a DFA with finite states.
This is more general than using the definition of `Language.IsRegular` directly, as the state type
`σ` is universe-polymorphic.
-/
theorem isRegular_iff {T : Type u} {L : Language T} :
L.IsRegular ↔ ∃ σ : Type v, ∃ _ : Fintype σ, ∃ M : DFA T σ, M.accepts = L :=
⟨Language.isRegular_iff.helper, Language.isRegular_iff.helper⟩
