α : Type u_1
β : Type u_2
γ : Type ?u.37999
ι : Sort ?u.38002
π : α → Type ?u.38007
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
p : Set γ
f✝ f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
s t u : Set α
f : α → β
h : s ∩ t = ∅
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
⊢ f '' s ∩ f '' t = ∅
α : Type u_1
β : Type u_2
γ : Type ?u.37999
ι : Sort ?u.38002
π : α → Type ?u.38007
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
p : Set γ
f✝ f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
s t u : Set α
f : α → β
h : Disjoint s t
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
⊢ Disjoint (f '' s) (f '' t)
rw [disjoint_iff_inter_eq_empty] at h ⊢
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.37999
ι : Sort ?u.38002
π : α → Type ?u.38007
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
p : Set γ
f✝ f₁ f₂ f₃ : α → β
g g₁ g₂ : β → γ
f' f₁' f₂' : β → α
g' : γ → β
a : α
b : β
s t u : Set α
f : α → β
h : s ∩ t = ∅
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
⊢ f '' s ∩ f '' t = ∅
rw [← hf.image_inter hs ht, h, image_empty]