forall₂_drop — Mathlib

English

For any n, if Forall₂ R l1 l2 holds, then Forall₂ R (drop n l1) (drop n l2) holds.

Русский

Для любого n, если Forall₂ R l1 l2 верно, то Forall₂ R (drop n l1) (drop n l2) верно.

LaTeX

$$$ \forall n,\ \mathrm{Forall₂}\ R\ l_1\ l_2\Rightarrow\mathrm{Forall₂}\ R\ (\mathrm{drop}\ n\ l_1)\ (\mathrm{drop}\ n\ l_2) $$$

Lean4

theorem forall₂_drop : ∀ (n) {l₁ l₂}, Forall₂ R l₁ l₂ → Forall₂ R (drop n l₁) (drop n l₂)
  | 0, _, _, h => by simp only [drop, h]
  | _ + 1, _, _, Forall₂.nil => by simp only [Forall₂.nil, drop]
  | n + 1, _, _, Forall₂.cons h₁ h₂ => by simp [And.intro h₁ h₂, forall₂_drop n]

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