head_val' — Mathlib

English

For any B: Fin m.succ × n' → α and fixed j, the first entry of the j-th column of the column vector B is the first entry of B in that column, i.e., the head of the column equals the head of B restricted to j.

Русский

Для любого B: Fin m.succ × n' → α и фиксированного j, первая запись j-го столбца в столбцовом векторе равна первой записи соответствующего столбца B, то есть голова столбца равна голове B для этого j.

LaTeX

$$$\\mathrm{vecHead}( (i \\mapsto B i j) ) = \\mathrm{vecHead} B j$$$

Lean4

@[simp]
theorem head_val' (B : Fin m.succ → n' → α) (j : n') : (vecHead fun i => B i j) = vecHead B j :=
  rfl

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