α : Type u_1
β : Type u_2
γ : Type ?u.47510
ι : Sort ?u.47513
ι' : Sort ?u.47516
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s t : Set α
⊢ f '' s ⊆ f '' (t ∪ s)
α : Type u_1
β : Type u_2
γ : Type ?u.47510
ι : Sort ?u.47513
ι' : Sort ?u.47516
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s t : Set α
⊢ f '' s \ f '' t ⊆ f '' (s \ t)
rw [diff_subset_iff, ← image_union, union_diff_self]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.47510
ι : Sort ?u.47513
ι' : Sort ?u.47516
f✝ : α → β
s✝ t✝ : Set α
f : α → β
s t : Set α
⊢ f '' s ⊆ f '' (t ∪ s)
exact image_subset f (subset_union_right t s)