fromCols_ext_iff — Mathlib

English

Two column-partitioned matrices are equal exactly when their corresponding left and right column blocks are equal: fromCols A1 A2 = fromCols B1 B2 iff A1 = B1 and A2 = B2.

Русский

Две матрицы, разделённые по столбцам, равны тогда и только тогда, когда их соответствующие левые и правые столбцы блоки равны: fromCols A1 A2 = fromCols B1 B2 ⇔ A1 = B1 и A2 = B2.

LaTeX

$$$$\operatorname{fromCols}(A_1,A_2)=\operatorname{fromCols}(B_1,B_2) \iff A_1=B_1 \wedge A_2=B_2.$$$$

Lean4

theorem fromCols_ext_iff (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (B₁ : Matrix m n₁ R) (B₂ : Matrix m n₂ R) :
    fromCols A₁ A₂ = fromCols B₁ B₂ ↔ A₁ = B₁ ∧ A₂ = B₂ :=
  fromCols_inj.eq_iff

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