reverse

Mathlib.Computability.NFA

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

← MathLib Explorer

English

If a language L is regular, then its reversal L.reverse is also regular.

Русский

Если язык L регулярный, то и обратный язык L.reverse регулярный.

LaTeX

$$L.IsRegular → L.reverse.IsRegular$$

Lean4

protected theorem reverse {L : Language α} (h : L.IsRegular) : L.reverse.IsRegular :=
  have ⟨σ, _, M, hM⟩ := h
  ⟨_, inferInstance, M.toNFA.reverse.toDFA, by ext; simp [hM]⟩

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

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

Разделы

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

Аффилиация

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