forall₂_zip — Mathlib

English

If Forall₂ R l1 l2 holds, then for any (a,b) in zip l1 l2 we have R a b.

Русский

Если Forall₂ R l1 l2 верно, то для любого (a,b) из zip l1 l2 выполняется R a b.

LaTeX

$$$ \forall {l_1 l_2},\mathrm{Forall₂}\ R\ l_1\ l_2\Rightarrow\forall {a\,b},\ (a,b) \in \mathrm{zip}\ l_1\ l_2\Rightarrow R\ a\ b $$$

Lean4

theorem forall₂_zip : ∀ {l₁ l₂}, Forall₂ R l₁ l₂ → ∀ {a b}, (a, b) ∈ zip l₁ l₂ → R a b
  | _, _, Forall₂.cons h₁ h₂, x, y, hx => by
    rw [zip, zipWith, mem_cons] at hx
    match hx with
    | Or.inl rfl => exact h₁
    | Or.inr h₃ => exact forall₂_zip h₂ h₃

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