map_injective_of_injective — Mathlib

English

If f is injective, then the map f is injective on LieSubmodules.

Русский

Если f инъективно, тогда отображение f инъективно на подмодулях Ли.

LaTeX

$$$ \text{hf : Injective } f \Rightarrow \text{Injective } (map f) $$$

Lean4

theorem map_injective_of_injective (hf : Function.Injective f) : Function.Injective (map f) := fun {N N'} h ↦
  SetLike.coe_injective <| hf.image_injective <| by simp only [← coe_map, h]

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