fromRows_map — Mathlib

English

Mapping a matrix by a function f distributes over the construction of a matrix partitioned by rows: map f applied to fromRows(A1,A2) equals fromRows(map f A1, map f A2).

Русский

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

LaTeX

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

Lean4

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

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