ι : Sort ?u.104386
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
⊢ ∃ a, f '' a = s
ι : Sort ?u.104386
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
⊢ Surjective (image f)
intro s
ι : Sort ?u.104386
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
⊢ f '' (f ⁻¹' s) = s
ι : Sort ?u.104386
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
⊢ ∃ a, f '' a = s
use f ⁻¹' s
no goals
ι : Sort ?u.104386
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
⊢ f '' (f ⁻¹' s) = s
rw [hf.image_preimage]