fromRows_toRows — Mathlib

English

Let A be a matrix with its rows partitioned into a top block A1 of size m1 and a bottom block A2 of size m2. Then the whole matrix equals the vertical concatenation fromRows(A1, A2). In other words, A = fromRows(A1, A2) where A1 = A.toRows₁ and A2 = A.toRows₂.

Русский

Пусть матрица A имеет верхнюю часть строк A1 размерности m1 и нижнюю часть строк A2 размерности m2. Тогда вся матрица равна вертикальному объединению fromRows(A1, A2). То есть A = fromRows(A1, A2) с A1 = A.toRows₁, A2 = A.toRows₂.

LaTeX

$$$$A = \operatorname{fromRows}(A_{\text{top}}, A_{\text{bottom}})$$$$

Lean4

@[simp]
theorem fromRows_toRows (A : Matrix (m₁ ⊕ m₂) n R) : fromRows A.toRows₁ A.toRows₂ = A := by ext (i | i) j <;> simp

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