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

State before:
A B : Type
f : A → B
Y : Set B
a : A
⊢ a ∈ inverse_image f Y ↔ f a ∈ Y
Tactic:
rfl
State after:
no goals