forall₂_take — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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