α : Type u_2
β : Type u_1
γ : Type ?u.61159
δ : Type ?u.61162
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s : Set β
h : α ≃ₜ β
⊢ IsCompact (↑(Homeomorph.symm h) '' s) ↔ IsCompact s
α : Type u_2
β : Type u_1
γ : Type ?u.61159
δ : Type ?u.61162
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s : Set β
h : α ≃ₜ β
⊢ IsCompact (↑h ⁻¹' s) ↔ IsCompact s
rw [← image_symm]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.61159
δ : Type ?u.61162
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s : Set β
h : α ≃ₜ β
⊢ IsCompact (↑(Homeomorph.symm h) '' s) ↔ IsCompact s
exact h.symm.isCompact_image