isRegular_iff_finite_range_leftQuotient

English

A language is regular if and only if the set of its left quotients is finite.

Русский

Язык является регулярным тогда и только тогда, когда множество его левых делителей конечно.

LaTeX

$$L.IsRegular ↔ (Set.range L.leftQuotient).Finite$$

Lean4

/-- **Myhill–Nerode theorem**. A language is regular if and only if the set of left quotients is finite.
-/
theorem isRegular_iff_finite_range_leftQuotient : L.IsRegular ↔ (Set.range L.leftQuotient).Finite :=
  ⟨IsRegular.finite_range_leftQuotient, .of_finite_range_leftQuotient⟩

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