α : Type u_1
β : Type u_2
γ : Type ?u.112000
inst✝ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t✝ : Finset β
a : α
b c : β
s t : Finset α
f : α → β
hf : Injective f
⊢ _root_.Disjoint (image f s) (image f t) ↔
    _root_.Disjoint (map { toFun := f, inj' := hf } s) (map { toFun := f, inj' := hf } t)
α : Type u_1
β : Type u_2
γ : Type ?u.112000
inst✝ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t✝ : Finset β
a : α
b c : β
s t : Finset α
f : α → β
hf : Injective f
⊢ _root_.Disjoint (image f s) (image f t) ↔ _root_.Disjoint s t
rw [←disjoint_map ⟨_, hf⟩]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.112000
inst✝ : DecidableEq β
f✝ g : α → β
s✝ : Finset α
t✝ : Finset β
a : α
b c : β
s t : Finset α
f : α → β
hf : Injective f
⊢ _root_.Disjoint (image f s) (image f t) ↔
    _root_.Disjoint (map { toFun := f, inj' := hf } s) (map { toFun := f, inj' := hf } t)
simp [map_eq_image]