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