reverse — Mathlib

English

If r.Rewrites u v, then r.reverse.Rewrites u.reverse v.reverse, i.e., reversing both sides preserves rewrites under reverse.

Русский

Если r.Rewrites u v, то r.reverse.Rewrites u.reverse v.reverse; разворот сохраняет переписывания.

LaTeX

$$$\forall {u v},\; r.Rewrites\ u\ v \Rightarrow r.reverse.Rewrites\ u.reverse\ v.reverse$$$

Lean4

protected theorem reverse : ∀ {u v}, r.Rewrites u v → r.reverse.Rewrites u.reverse v.reverse
  | _, _, head s => by simpa using .append_left .input_output _
  | _, _, @cons _ _ _ x u v h => by simpa using h.reverse.append_right _

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