Theorem: HTPI.inv_comp (HTPILib/Chap8Part1.lean)

State before:
U V W : Type
R : Rel U V
S : Rel V W
⊢ invRel (compRel S R) = RelFromExt (inv (comp (extension S) (extension R)))
Tactic:
rfl
State after:
no goals

State before:
U V W : Type
R : Rel U V
S : Rel V W
⊢ RelFromExt (inv (comp (extension S) (extension R))) = RelFromExt (comp (inv (extension R)) (inv (extension S)))
Tactic:
rw [Theorem_4_2_5_5]
State after:
no goals

State before:
U V W : Type
R : Rel U V
S : Rel V W
⊢ RelFromExt (comp (inv (extension R)) (inv (extension S))) = compRel (invRel R) (invRel S)
Tactic:
rfl
State after:
no goals