tail_val' — Mathlib

English

For B as above and fixed j, the tail of the column given by B equals the column formed by taking the tails of B entrywise, i.e., the tail of the j-th column is vecTail B i j as a function of i.

Русский

Для данного B и фиксированного j хвост столбца равен столбцу, составленному из хвостов B по строкам: хвост j-го столбца равен vecTail B i j как функция от i.

LaTeX

$$$\\mathrm{vecTail}( \\lambda i. B i j ) = \\lambda i. \\mathrm{vecTail} B i j$$$

Lean4

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

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