α : Type u
β : Type v
γ : Type w
δ : Type ?u.221604
ι : Sort x
f : Filter α
m : α → β
m' : β → γ
s : Set α
t : Set β
⊢ m '' univ ∈ map m f
α : Type u
β : Type v
γ : Type w
δ : Type ?u.221604
ι : Sort x
f : Filter α
m : α → β
m' : β → γ
s : Set α
t : Set β
⊢ range m ∈ map m f
rw [← image_univ]
no goals
α : Type u
β : Type v
γ : Type w
δ : Type ?u.221604
ι : Sort x
f : Filter α
m : α → β
m' : β → γ
s : Set α
t : Set β
⊢ m '' univ ∈ map m f
exact image_mem_map univ_mem