fromRows_apply_inr — Mathlib

English

For A1, A2 of compatible sizes, the values of fromRows at Sum.inl i and Sum.inr i agree with A1 i and A2 i respectively.

Русский

Для A1 и A2 допустимых размеров значения fromRows на Sum.inl i и Sum.inr i совпадают с A1 i и A2 i соответственно.

LaTeX

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

Lean4

@[simp]
theorem fromRows_apply_inr (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (i : m₂) (j : n) :
    (fromRows A₁ A₂) (Sum.inr i) j = A₂ i j :=
  rfl

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