invRev — Mathlib

English

If L1 reduces to L2 in the reduction relation, then invRev L1 reduces to invRev L2 as well.

Русский

Если L1 редуцируется до L2 в отношении редукции, то invRev L1 редуцируется до invRev L2.

LaTeX

$$$\\forall L_1,L_2\\, Red\\, L_1\\ L_2 \\Rightarrow Red\\ (invRev\\ L_1)\\ (invRev\\ L_2)$$$

Lean4

@[to_additive]
theorem invRev {L₁ L₂ : List (α × Bool)} (h : Red L₁ L₂) : Red (invRev L₁) (invRev L₂) :=
  Relation.ReflTransGen.lift _ (fun _a _b => Red.Step.invRev) h

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