produces_reverse_comm — Mathlib

English

The Produces relation is intertwined with reversal: g.reverse.Produces(u, v) is equivalent to g.Produces(u.reverse, v.reverse).

Русский

Связь Produces связана с разворотом: g.reverse.Produces(u, v) эквивалентно g.Produces(u.reverse, v.reverse).

LaTeX

$$$ g.reverse.Produces\bigl(u, v\bigr) \iff g.Produces\bigl(u.reverse, v.reverse\bigr) $$$

Lean4

@[simp]
theorem produces_reverse_comm : g.reverse.Produces u v ↔ g.Produces u.reverse v.reverse :=
  (Equiv.ofBijective _ ContextFreeRule.reverse_bijective).exists_congr
    (by simp [ContextFreeRule.reverse_involutive.eq_iff])

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