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