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

State before:
A B : Type
f : A → B
X : Set A
b : B
⊢ b ∈ image f X ↔ ∃ x ∈ X, f x = b
Tactic:
rfl
State after:
no goals