range — Mathlib

English

If L M is finitely generated, then the image under any L-homomorphism f:M→[L]N is finitely generated as an L-structure on N.

Русский

Если L-структура M порождена конечным образом, то образ под любым тождественным гомоморфизмом f:M→[L]N также порождается конечным образом.

LaTeX

$$$\text{FG}(L,M) \rightarrow \text{FG}(L,\operatorname{range}(f))$$$

Lean4

theorem range {N : Type*} [L.Structure N] (h : FG L M) (f : M →[L] N) : f.range.FG :=
  by
  rw [Hom.range_eq_map]
  exact (fg_def.1 h).map f

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