ι : Sort ?u.104645
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s t : Set α
h : f '' s = f '' t
⊢ s = t
ι : Sort ?u.104645
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
⊢ Injective (image f)
intro s t h
no goals
ι : Sort ?u.104645
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s t : Set α
h : f '' s = f '' t
⊢ s = t
rw [← preimage_image_eq s hf, ← preimage_image_eq t hf, h]