lean_workbook_plus_24996

Proved

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

Prove that if there exists a function $g: Y\to X$ such that $f\circ g = I_{Y}$ , then $f$ is a surjection.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_24996 {X Y: Type} {f : X → Y} (g : Y → X) (h₁ : f ∘ g = id) : Function.Surjective f   :=  by sorry

Source