of_finite_range_leftQuotient

Mathlib.Computability.MyhillNerode

URI: https://scilib.ai/kg/mathlib#Language.IsRegular.of_finite_range_leftQuotient

← MathLib Explorer

English

If the range of leftQuotient is finite, then L is regular.

Русский

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

LaTeX

$$(L.leftQuotient).range.Finite → L.IsRegular$$

Lean4

theorem of_finite_range_leftQuotient (h : Set.Finite (Set.range L.leftQuotient)) : L.IsRegular :=
  Language.isRegular_iff.mpr ⟨_, h.fintype, L.toDFA, by simp⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru