fromCols — Mathlib

English

Concatenate two matrices B1 (m × n1) and B2 (m × n2) with the same rows to form a larger matrix of size m × (n1 ⊕ n2), by stacking B1 and B2 side by side.

Русский

Соединяем две матрицы B1 (m × n1) и B2 (m × n2) по строкам, получая матрицу размера m × (n1 ⊕ n2).

LaTeX

$$$\\text{fromCols}(B_1,B_2) = B_1 \\oplus B_2$$$

Lean4

/-- Concatenate together two matrices B₁[m × n₁] and B₂[m × n₂] with the same rows (M) to get a
bigger matrix indexed by [m × (n₁ ⊕ n₂)] -/
def fromCols (B₁ : Matrix m n₁ R) (B₂ : Matrix m n₂ R) : Matrix m (n₁ ⊕ n₂) R :=
  of fun i => Sum.elim (B₁ i) (B₂ i)

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