fromRows_ext_iff — Mathlib

English

Two row-partitioned matrices are equal exactly when their corresponding top and bottom row blocks are equal: fromRows A1 A2 = fromRows B1 B2 iff A1 = B1 and A2 = B2.

Русский

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

LaTeX

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

Lean4

theorem fromRows_ext_iff (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (B₁ : Matrix m₁ n R) (B₂ : Matrix m₂ n R) :
    fromRows A₁ A₂ = fromRows B₁ B₂ ↔ A₁ = B₁ ∧ A₂ = B₂ :=
  fromRows_inj.eq_iff

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