Theorem: Section3sheet1.surjective_def (FormalisingMathematics2024/Section03functions/Sheet1.lean)

State before:
X Y Z : Type
f : X → Y
⊢ Surjective f ↔ ∀ (b : Y), ∃ a, f a = b
Tactic:
rfl
State after:
no goals