matrix_map — Mathlib

English

If f is a closed embedding, then the entrywise matrix map is a closed embedding.

Русский

Если f — замкнутое вложение, то отображение матриц по элементам является замкнутым вложением.

LaTeX

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

Lean4

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

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