matrix_map — Mathlib

English

If f is an inducing map, then applying f entrywise to matrices yields an inducing map on matrix-valued inputs.

Русский

Если f — индукционирующее отображение, то применение f по каждому коэффициенту к матрицам порождает индукционирующее отображение между пространствами матриц.

LaTeX

$$$\\operatorname{IsInducing}(f) \\Rightarrow \\operatorname{IsInducing}\\bigl(\\operatorname{map}\\,\\cdot\\, f : \\text{Matrix}_{m\\times n}(R) \\to \\text{Matrix}_{m\\times n}(S)\\bigr)$$$

Lean4

theorem matrix_map (hf : IsInducing f) : IsInducing (map · f : Matrix m n R → Matrix m n S) :=
  IsInducing.piMap fun _ : m ↦ (IsInducing.piMap fun _ : n ↦ hf)

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