English
If f is surjective, then any y in the image of I under f actually comes from some x in I; equivalently, every element of the ideal map is realized as f x with x ∈ I.
Русский
Пусть f сюръективно. Любой элемент y из I под отображением f получен как f x для некоторого x ∈ I.
LaTeX
$$$hf : \mathrm{Function.Surjective}(f) \rightarrow \forall I \in \mathrm{Ideal}(R), \forall y \in S,\; y \in \mathrm{Ideal.map}(f,I) \Rightarrow \exists x \in I, f x = y$$$
Lean4
theorem mem_image_of_mem_map_of_surjective {I : Ideal R} {y} (H : y ∈ map f I) : y ∈ f '' I :=
Submodule.span_induction (hx := H) (fun _ => id) ⟨0, I.zero_mem, map_zero f⟩
(fun _ _ _ _ ⟨x1, hx1i, hxy1⟩ ⟨x2, hx2i, hxy2⟩ => ⟨x1 + x2, I.add_mem hx1i hx2i, hxy1 ▸ hxy2 ▸ map_add f _ _⟩)
fun c _ _ ⟨x, hxi, hxy⟩ =>
let ⟨d, hdc⟩ := hf c
⟨d * x, I.mul_mem_left _ hxi, hdc ▸ hxy ▸ map_mul f _ _⟩
