forall₂_of_length_eq_of_get — Mathlib

English

If length equality holds and every corresponding pair satisfies R, then Forall₂ R holds for the lists.

Русский

Если длина списков равна и каждая пара элементов удовлетворяет R, то Forall₂ R выполняется для списков.

LaTeX

$$$ \text{length equality and pointwise }R\Rightarrow \mathrm{Forall₂}\ R\ x\ y. $$$$

Lean4

theorem forall₂_of_length_eq_of_get :
    ∀ {x : List α} {y : List β}, x.length = y.length → (∀ i h₁ h₂, R (x.get ⟨i, h₁⟩) (y.get ⟨i, h₂⟩)) → Forall₂ R x y
  | [], [], _, _ => Forall₂.nil
  | _ :: _, _ :: _, hl, h =>
    Forall₂.cons (h 0 (Nat.zero_lt_succ _) (Nat.zero_lt_succ _))
      (forall₂_of_length_eq_of_get (succ.inj hl) fun i h₁ h₂ => h i.succ (succ_lt_succ h₁) (succ_lt_succ h₂))

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