mem_map_iff_of_surjective — Mathlib

English

Let f be surjective. For any ideal I of R and any y in S, y ∈ map f I iff there exists x ∈ I with f x = y.

Русский

Пусть f сюръективно. Тогда для любого идеала I в R и любого y в S: y ∈ map f I эквивалентно существованию x ∈ I с f x = y.

LaTeX

$$$hf : \mathrm{Function.Surjective}(f) \rightarrow \forall {I : \mathrm{Ideal}(R)} {y : S}, \; y \in \mathrm{Ideal.map}(f I) \ \Leftrightarrow \ \exists x \in I, f x = y$$$

Lean4

theorem mem_map_iff_of_surjective {I : Ideal R} {y} : y ∈ map f I ↔ ∃ x, x ∈ I ∧ f x = y :=
  ⟨fun h => (Set.mem_image _ _ _).2 (mem_image_of_mem_map_of_surjective f hf h), fun ⟨_, hx⟩ =>
    hx.right ▸ mem_map_of_mem f hx.left⟩

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