reindex — Mathlib

English

Let g: σ ≃ σ' be a bijection between state sets. Then renaming the states of any DFA M by g yields a DFA that is canonically equivalent to M; in particular there is a canonical isomorphism between DFA α σ and DFA α σ' given by reindex g, with inverse given by reindex g^{-1}.

Русский

Пусть g: σ ≃ σ' — биекция между множествами состояний. Переиндексация состояний DFA M по g даёт DFA, изоморфный M; существуют взаимно однозначные отображения между DFA α σ и DFA α σ' через переиндексацию g и её обратную.

LaTeX

$$$ \\forall g:\\sigma\\simeq\\sigma',\\ DFA(\\alpha,\\sigma) \\cong DFA(\\alpha,\\sigma') $$$

Lean4

/-- Lifts an equivalence on states to an equivalence on DFAs. -/
@[simps apply_step apply_start apply_accept]
def reindex (g : σ ≃ σ') : DFA α σ ≃ DFA α σ'
    where
  toFun
    M :=
    { step := fun s a => g (M.step (g.symm s) a)
      start := g M.start
      accept := g.symm ⁻¹' M.accept }
  invFun
    M :=
    { step := fun s a => g.symm (M.step (g s) a)
      start := g.symm M.start
      accept := g ⁻¹' M.accept }
  left_inv M := by simp
  right_inv M := by simp

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