fromRows — Mathlib

English

Concatenate two matrices A1 (m1 × N) and A2 (m2 × N) with the same columns to form a larger matrix of size (m1 ⊕ m2) × N, by stacking A1 above A2.

Русский

Соединяем две матрицы A1 (m1 × N) и A2 (m2 × N) с одинаковыми столбцами в большую матрицу размера (m1 ⊕ m2) × N, помещая A1 сверху A2.

LaTeX

$$$\\text{fromRows}(A_1,A_2) = \\begin{pmatrix} A_1 \\\\ A_2 \\end{pmatrix}$$$

Lean4

/-- Concatenate together two matrices A₁[m₁ × N] and A₂[m₂ × N] with the same columns (N) to get a
bigger matrix indexed by [(m₁ ⊕ m₂) × N] -/
def fromRows (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) : Matrix (m₁ ⊕ m₂) n R :=
  of (Sum.elim A₁ A₂)

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