seq_eq — Mathlib

English

For all m, f, v, we have seq f v = fun i => f i (v i).

Русский

Для всех m, f, v выполняется seq f v = fun i => f i (v i).

LaTeX

$$$\mathrm{seq}(f,v) = \lambda i. f(i)(v(i))$$$

Lean4

@[simp]
theorem seq_eq : ∀ {m} (f : Fin m → α → β) (v : Fin m → α), seq f v = fun i => f i (v i)
  | 0, _, _ => Subsingleton.elim _ _
  | n + 1, f, v =>
    funext fun i => by
      simp_rw [seq, seq_eq]
      refine i.cases ?_ fun i => ?_
      · rfl
      · rw [Matrix.cons_val_succ]
        rfl

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