Prove2Me

Direct_Image_Mapping_of_Surjection_is_Surjection

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

direct-image-mappingspower-setproofwikisurjections

Let f: S → T be a surjection. Then the direct image mapping of f, f→: đ’«(S) → đ’«(T), is a surjection.

Preamble
import Mathlib.Data.Set.Function
Formal statement
theorem Direct_Image_Mapping_of_Surjection_is_Surjection {α : Type _} {ÎČ : Type _} {f : α → ÎČ} (hf : Function.Surjective f) : Function.Surjective (Set.image f) := by sorry
Source
https://proofwiki.org/wiki/Direct_Image_Mapping_of_Surjection_is_Surjection

View graph