fromCols_map — Mathlib

English

Mapping a function f distributes over the construction of a matrix partitioned by columns: map f (fromCols(A1,A2)) = fromCols(map f A1, map f A2).

Русский

Отображение по функции f распространяется на разбиение матрицы по столбцам: map f (fromCols(A1,A2)) = fromCols(map f A1, map f A2).

LaTeX

$$$$ (\operatorname{fromCols}(A_1,A_2)).\operatorname{map} f = \operatorname{fromCols}(A_1.\operatorname{map} f)(A_2.\operatorname{map} f). $$$$

Lean4

theorem fromCols_map (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) {R' : Type*} (f : R → R') :
    (fromCols A₁ A₂).map f = fromCols (A₁.map f) (A₂.map f) := by ext _ (_ | _) <;> rfl

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