derives_reverse_comm — Mathlib

English

Reversing both sides yields the same Derives relation in opposite direction: g.reverse.Derives(u, v) iff g.Derives(u.reverse, v.reverse).

Русский

Разворот сохраняет направление Derives в обратном виде: g.reverse.Derives(u, v) эквивалентно g.Derives(u.reverse, v.reverse).

LaTeX

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

Lean4

@[simp]
theorem derives_reverse_comm : g.reverse.Derives u v ↔ g.Derives u.reverse v.reverse := by
  rw [iff_comm, ← derives_reverse, List.reverse_reverse, List.reverse_reverse]

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