get — Mathlib

English

If Forall₂ R x y holds, then for every index i with i < |x| and i < |y|, R (x.get i) (y.get i).

Русский

Если Forall₂ R x y, то для каждого i с i < |x| и i < |y| выполняется R (x.i) (y.i).

LaTeX

$$$ \mathrm{Forall₂}\ R\ x\ y \Rightarrow\forall i\ (h_x:\ i<|x|) (h_y:\ i<|y|),\ R\ (x.\mathrm{get}\langle i,h_x\rangle)\ (y.\mathrm{get}\langle i,h_y\rangle) $$$

Lean4

theorem get :
    ∀ {x : List α} {y : List β},
      Forall₂ R x y → ∀ ⦃i : ℕ⦄ (hx : i < x.length) (hy : i < y.length), R (x.get ⟨i, hx⟩) (y.get ⟨i, hy⟩)
  | _, _, Forall₂.cons ha _, 0, _, _ => ha
  | _, _, Forall₂.cons _ hl, succ _, _, _ => hl.get _ _

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