submatrix_empty — Mathlib

English

For any matrix A, the submatrix obtained by selecting an empty set of rows is the empty matrix.

Русский

Для любой матрицы A подматрица, полученная из пустого набора строк, есть пустая матрица.

LaTeX

$$$A\.submatrix(\text{row} :\mathrm{Fin}0 \to m', \text{col}: o' \to n') = \![]$$$

Lean4

@[simp]
theorem submatrix_empty (A : Matrix m' n' α) (row : Fin 0 → m') (col : o' → n') : submatrix A row col = ![] :=
  empty_eq _

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