Theorem: HTPI.graph_def (HTPILib/Chap5.lean)

State before:
A B : Type
f : A → B
a : A
b : B
⊢ (a, b) ∈ graph f ↔ f a = b
Tactic:
rfl
State after:
no goals