mem_accepts_reverse — Mathlib

English

Membership of a word in the reverse automaton's accepts corresponds to membership of the reversed word in the original automaton's accepts.

Русский

Членство слова в принятии обратного автомата эквивалентно членству развёрнутого слова в принятии исходного автомата.

LaTeX

$$x ∈ M.reverse.accepts ↔ x.reverse ∈ M.accepts$$

Lean4

@[simp]
theorem mem_accepts_reverse {x : List α} : x ∈ M.reverse.accepts ↔ x.reverse ∈ M.accepts := by
  simp [mem_accepts, ← Set.not_disjoint_iff, disjoint_evalFrom_reverse_iff]

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