map_injective — Mathlib

English

If f is injective, then the map M ↦ M.map f is injective on CStarMatrix m n A.

Русский

Если f инъективен, отображение M ↦ M.map f инъективно на пространства матриц.

LaTeX

$$$(hf : \text{Function.Injective } f) \\Rightarrow \\text{Injective } (\\lambda M : CStarMatrix m n A, M.map f)$$$

Lean4

theorem map_injective {f : A → B} (hf : Function.Injective f) :
    Function.Injective fun M : CStarMatrix m n A => M.map f := fun _ _ h => ext fun i j => hf <| ext_iff.mpr h i j

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