invRev — Mathlib

English

If a single reduction step reduces L1 to L2, then applying invRev to both sides yields a valid reduction step from invRev L1 to invRev L2.

Русский

Если за счёт одной редукционной стадии L1 переходит в L2, то применение invRev к обеим сторонам даёт редукционный шаг от invRev L1 к invRev L2.

LaTeX

$$$\\forall L_1,L_2,\\; Red.Step\\ L_1\\ L_2 \\Rightarrow Red.Step\\ (invRev\\ L_1)\\ (invRev\\ L_2)$$$

Lean4

@[to_additive]
theorem invRev {L₁ L₂ : List (α × Bool)} (h : Red.Step L₁ L₂) : Red.Step (FreeGroup.invRev L₁) (FreeGroup.invRev L₂) :=
  by
  obtain ⟨a, b, x, y⟩ := h
  simp [FreeGroup.invRev]

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