map — Mathlib

English

If the image of a finitely generated substructure under an embedding is finitely generated, then the original is finitely generated.

Русский

Если образ конечнопорождаемой подструктуры под вложением остается конечнопорождаемым, то исходная тоже конечнопорождаемая.

LaTeX

$$$(s.map f).FG \Rightarrow s.FG$$$

Lean4

theorem map {N : Type*} [L.Structure N] (f : M →[L] N) {s : L.Substructure M} (hs : s.FG) : (s.map f).FG :=
  let ⟨t, ht⟩ := fg_def.1 hs
  fg_def.2 ⟨f '' t, ht.1.image _, by rw [closure_image, ht.2]⟩

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