α : Type u_1
β : Type u_2
γ : Type ?u.70476
ι : Sort ?u.70479
ι' : Sort ?u.70482
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set α
⊢ f '' s ⊆ f '' univ
α : Type u_1
β : Type u_2
γ : Type ?u.70476
ι : Sort ?u.70479
ι' : Sort ?u.70482
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set α
⊢ f '' s ⊆ range f
rw [← image_univ]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.70476
ι : Sort ?u.70479
ι' : Sort ?u.70482
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set α
⊢ f '' s ⊆ f '' univ
exact image_subset _ (subset_univ _)