fromCols_apply_inl — Mathlib

English

The operation fromCols combines A1 and A2 by columns; the left block equals A1 on Sum.inl indices and the right block equals A2 on Sum.inr indices.

Русский

Операция fromCols объединяет A1 и A2 по столбцам: левая часть равна A1 на индексах Sum.inl, правая — A2 на Sum.inr.

LaTeX

$$$(\\text{fromCols}(A_1,A_2)) i (\\text{Sum.inl } j) = A_1 i j$$$

Lean4

@[simp]
theorem fromCols_apply_inl (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (i : m) (j : n₁) :
    (fromCols A₁ A₂) i (Sum.inl j) = A₁ i j :=
  rfl

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