English
In a (u+d) × (l+r) matrix A, the bottom-left block has size d × l and consists of the last d rows and first l columns; its entries satisfy ((subDownLeft A))_{i j} = A_{u+i, j} for i ∈ Fin(d), j ∈ Fin(l).
Русский
В матрице размером (u+d) × (l+r) нижняя левая подматрица имеет размер d × l и состоит из последних d строк и первых l столбцов; её элементы удовлетворяют ((subDownLeft A))_{i j} = A_{u+i, j}.
LaTeX
$$$((\text{subDownLeft } A))_{i j} = A_{u+i,\, j}$ for all $i \in \operatorname{Fin}(d)$, $j \in \operatorname{Fin}(l)$$$
Lean4
/-- The bottom-left `d × l` part of a `(u+d) × (l+r)` matrix. -/
abbrev subDownLeft {d u l r : Nat} (A : Matrix (Fin (u + d)) (Fin (l + r)) α) : Matrix (Fin d) (Fin l) α :=
subDown (subLeft A)
