map_le_range — Mathlib

English

For any submodule p, the image under f of p is always contained in the range of f: map f p ≤ range f.

Русский

Для любого подмодуля p образ через f содержится в диапазоне f: map f p ≤ range f.

LaTeX

$$$\operatorname{map} f\, p \le \operatorname{range} f$$$

Lean4

theorem map_le_range [RingHomSurjective τ₁₂] {f : F} {p : Submodule R M} : map f p ≤ range f :=
  SetLike.coe_mono (Set.image_subset_range f p)

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