α : Type u
β : Type v
ι : Type ?u.90314
π : ι → Type ?u.90319
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : CompactSpace α
f : α → β
hf : Continuous f
⊢ IsCompact (f '' univ)
α : Type u
β : Type v
ι : Type ?u.90314
π : ι → Type ?u.90319
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : CompactSpace α
f : α → β
hf : Continuous f
⊢ IsCompact (range f)
rw [← image_univ]
no goals
α : Type u
β : Type v
ι : Type ?u.90314
π : ι → Type ?u.90319
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
s t : Set α
inst✝ : CompactSpace α
f : α → β
hf : Continuous f
⊢ IsCompact (f '' univ)
exact isCompact_univ.image hf