matrix_map — Mathlib

English

If f is an open embedding, then the entrywise matrix map is an open embedding (under finiteness assumptions).

Русский

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

LaTeX

$$$\\operatorname{Finite}(m) \\land \\operatorname{Finite}(n) \\land \\operatorname{IsOpenEmbedding}(f) \\Rightarrow \\operatorname{IsOpenEmbedding}(\\lambda x. x.map f)$$$

Lean4

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

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