forall₂_reverse_iff — Mathlib

English

Forall₂ R on reversed lists is equivalent to Forall₂ R on the original lists.

Русский

Для списка в обратном порядке Forall₂ R эквивалентно Forall₂ R на исходных списках.

LaTeX

$$$ \mathrm{forall\_₂\_reverse\_iff} :\ Forall₂\ R\ l_1\ l_2 \;\Leftrightarrow\; \mathrm{Forall₂}\ R\ l_1\ l_2 $$$

Lean4

@[simp]
theorem forall₂_reverse_iff {l₁ l₂} : Forall₂ R (reverse l₁) (reverse l₂) ↔ Forall₂ R l₁ l₂ :=
  Iff.intro
    (fun h => by
      rw [← reverse_reverse l₁, ← reverse_reverse l₂]
      exact rel_reverse h)
    fun h => rel_reverse h

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