rel_reverse — Mathlib

English

Forall₂ R is preserved by reversing lists: If Forall₂ R a b, then Forall₂ R (reverse a) (reverse b).

Русский

Forall₂ R сохраняется при отражении списков: если Forall₂ R a b, то Forall₂ R (reverse a) (reverse b).

LaTeX

$$$ \text{rel\_reverse} :\ (Forall₂\ R \Rightarrow Forall₂\ R)\ \mathrm{reverse}\ \mathrm{reverse}$$$

Lean4

theorem rel_reverse : (Forall₂ R ⇒ Forall₂ R) reverse reverse
  | [], [], Forall₂.nil => Forall₂.nil
  | _, _, Forall₂.cons h₁ h₂ => by
    simp only [reverse_cons]
    exact rel_append (rel_reverse h₂) (Forall₂.cons h₁ Forall₂.nil)

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