accepts_comap — Mathlib

English

The accepts set of the comapped DFA equals the preimage under map f of the accepts of M: (M.comap f).accepts = { x : List α' | x.map f ∈ M.accepts }.

Русский

Множество принятия для развёрнутого через f ДФА есть предварение по отображению map f от множества принятых состояний M.

LaTeX

$$$ (M.{\mathrm{comap}}\, f).\mathrm{accepts} = f^{-1}[M.\mathrm{accepts}] $$$

Lean4

@[simp]
theorem accepts_comap (f : α' → α) : (M.comap f).accepts = List.map f ⁻¹' M.accepts :=
  by
  ext x
  conv =>
    rhs
    rw [Set.mem_preimage, mem_accepts]
  simp [mem_accepts]

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