fromCols_inj — Mathlib

English

The operation of forming a matrix by placing two column blocks side by side is injective in each argument: if fromCols(A1, A2) = fromCols(B1, B2) then A1 = B1 and A2 = B2.

Русский

Операция формирования матрицы путем размещения двух блоков по столбцам инъективна по каждому аргументу: если fromCols(A1,A2) = fromCols(B1,B2), тогда A1 = B1 и A2 = B2.

LaTeX

$$$$\operatorname{fromCols}\text{-}\text{injective}:\quad \forall A_1,A_2,B_1,B_2,\; \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_inj : Function.Injective2 (@fromCols R m n₁ n₂) :=
  by
  intro x1 x2 y1 y2
  simp only [← Matrix.ext_iff]
  simp_all

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