Surjection_Induced_by_Powerset_is_Induced_by_Surjection
Proveddirect-image-mappingsproofwikisurjections
If the direct image mapping of a function f is surjective, then f itself is surjective.
Preamble
import Mathlib.Data.Set.Function
Formal statement
theorem Surjection_Induced_by_Powerset_is_Induced_by_Surjection {α : Type _} {β : Type _} {f : α → β} (hf : Function.Surjective (Set.image f)) : Function.Surjective f := by sorrySource