Theorem: HTPI.Theorem_4_2_5_2 (HTPILib/Chap4.lean)

State before:
A B : Type
R : Set (A × B)
⊢ Dom (inv R) = Ran R
Tactic:
rfl
State after:
no goals