reduce_invRev — Mathlib

English

The reduction commutes with inverse-reversal: reducing the inverse-reverse of a word equals the inverse-reverse of the reduction.

Русский

Редукция commuting с обратной операцией разворота: редукция инверсной развёртки слова равна развёртке редукции слова.

LaTeX

$$$\mathrm{reduce}(\mathrm{invRev}(w)) = \mathrm{invRev}(\mathrm{reduce}(w))$$$

Lean4

@[to_additive]
theorem reduce_invRev {w : List (α × Bool)} : reduce (invRev w) = invRev (reduce w) :=
  by
  apply reduce.min
  rw [← red_invRev_iff, invRev_invRev]
  apply Red.reduce_left
  have : Red (invRev (invRev w)) (invRev (reduce (invRev w))) := reduce.red.invRev
  rwa [invRev_invRev] at this

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