reverse_perm' — Mathlib

English

For any lists l1, l2, l1.reverse is Perm l2 iff l1 is Perm l2.reverse.

Русский

Для любых списков l1, l2, l1.reverse перестановочно эквивалентен l2 тогда, когда l1 перестановочно эквивален l2.reverse.

LaTeX

$$$ l_1^{\\\\text{reverse}} \\\\sim l_2 \\\\iff l_1 \\\\sim l_2^{\\\\text{reverse}} $$$

Lean4

@[simp]
theorem reverse_perm' : l₁.reverse ~ l₂ ↔ l₁ ~ l₂
    where
  mp := l₁.reverse_perm.symm.trans
  mpr := l₁.reverse_perm.trans

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