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

State before:
A B : Type
R : Set (A × B)
a : A
b : B
⊢ (b, a) ∈ inv R ↔ (a, b) ∈ R
Tactic:
rfl
State after:
no goals