map_le_range — Mathlib

English

For any LieModuleHom f, the image of a submodule under map f lies within the range of f.

Русский

Для любого гомоморфа модуля Ли образ подмодуля по отображению f лежит в диапазоне f.

LaTeX

$$$\operatorname{map}(f,N) \le \operatorname{range}(f)$$$

Lean4

@[simp]
theorem map_le_range {M' : Type*} [AddCommGroup M'] [Module R M'] [LieRingModule L M'] (f : M →ₗ⁅R,L⁆ M') :
    N.map f ≤ f.range := by
  rw [← LieModuleHom.map_top]
  exact LieSubmodule.map_mono le_top

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