forall₂_iff_get — Mathlib

English

Forall₂ R l1 l2 is equivalent to (length equality) and (pointwise get compatibility).

Русский

Forall₂ R l1 l2 эквивалентно (равенство длин) и (совместимость по элементам через get).

LaTeX

$$$ \forall {l_1}\ {l_2}:\ Forall₂ R l_1 l_2 \iff (\mathrm{length}\ l_1 = \mathrm{length}\ l_2) \land \forall i\ h_1\ h_2,\ R(l_1.\mathrm{get}\langle i,h_1\rangle)(l_2.\mathrm{get}\langle i,h_2\rangle) $$$

Lean4

theorem forall₂_iff_get {l₁ : List α} {l₂ : List β} :
    Forall₂ R l₁ l₂ ↔ l₁.length = l₂.length ∧ ∀ i h₁ h₂, R (l₁.get ⟨i, h₁⟩) (l₂.get ⟨i, h₂⟩) :=
  ⟨fun h => ⟨h.length_eq, h.get⟩, fun h => forall₂_of_length_eq_of_get h.1 h.2⟩

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