English
Let A be a matrix of size (u+d) × (l+r) partitioned into four blocks. The top-right block is the u × r submatrix consisting of the first u rows and the last r columns; its entries are given by ((subUpRight A))_{i j} = A_{i, l+j} for i = 0,…,u−1 and j = 0,…,r−1.
Русский
Пусть A — матрица размером (u+d) × (l+r), разбитая на четыре блока. Верхняя правая часть размером u × r состоит из первых u строк и последних r столбцов; её элементы задаются как ((subUpRight A))_{i j} = A_{i, l+j} для i = 0,…,u−1 и j = 0,…,r−1.
LaTeX
$$$((\text{subUpRight } A))_{i j} = A_{i,\, l+j}$ for all $i \in \operatorname{Fin}(u)$, $j \in \operatorname{Fin}(r)$$$
Lean4
/-- The top-right `u × r` part of a `(u+d) × (l+r)` matrix. -/
abbrev subUpRight {d u l r : Nat} (A : Matrix (Fin (u + d)) (Fin (l + r)) α) : Matrix (Fin u) (Fin r) α :=
subUp (subRight A)
