subLeft — Mathlib

English

The top u×n part of a (u+d)×n matrix is the submatrix obtained by restricting the row indices to the first u rows.

Русский

Верхняя часть матрицы размером (u+d)×n определяется как подматрица, ограничивающая строки первыми u рядами.

LaTeX

$$$ \text{subUp} (A) = \text{submatrix}(A, \mathrm{castAdd}(d), \mathrm{id}) $$$

Lean4

/-- The left `n × l` part of an `n × (l+r)` matrix. -/
abbrev subLeft {m l r : Nat} (A : Matrix (Fin m) (Fin (l + r)) α) : Matrix (Fin m) (Fin l) α :=
  submatrix A id (Fin.castAdd r)

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