lean_workbook_plus_14416

Proved

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

A function $s: A \to B$ is called a surjective function if $\forall b \in B$ , exists $a \in A$ such that $b=s(a)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_14416 {A B : Type} (s : A → B) : (∀ b : B, ∃ a : A, b = s a) ↔ Function.Surjective s   :=  by sorry

Source