Theorem: injective_def (FM2023Exrcise/section03_functions/sheet1.lean)

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