α : Type u_1
β : Type u_2
γ : Type ?u.104526
δ : Type ?u.104529
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CompactSpace α
inst✝ : T2Space β
f : α ≃ β
hf : Continuous ↑f
⊢ ∀ (s : Set α), IsClosed s → IsClosed (↑f.symm ⁻¹' s)
α : Type u_1
β : Type u_2
γ : Type ?u.104526
δ : Type ?u.104529
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CompactSpace α
inst✝ : T2Space β
f : α ≃ β
hf : Continuous ↑f
⊢ Continuous ↑f.symm
rw [continuous_iff_isClosed]
α : Type u_1
β : Type u_2
γ : Type ?u.104526
δ : Type ?u.104529
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CompactSpace α
inst✝ : T2Space β
f : α ≃ β
hf : Continuous ↑f
C : Set α
hC : IsClosed C
⊢ IsClosed (↑f.symm ⁻¹' C)
α : Type u_1
β : Type u_2
γ : Type ?u.104526
δ : Type ?u.104529
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CompactSpace α
inst✝ : T2Space β
f : α ≃ β
hf : Continuous ↑f
⊢ ∀ (s : Set α), IsClosed s → IsClosed (↑f.symm ⁻¹' s)
intro C hC
α : Type u_1
β : Type u_2
γ : Type ?u.104526
δ : Type ?u.104529
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CompactSpace α
inst✝ : T2Space β
f : α ≃ β
hf : Continuous ↑f
C : Set α
hC : IsClosed C
hC' : IsClosed (↑f '' C)
⊢ IsClosed (↑f.symm ⁻¹' C)
α : Type u_1
β : Type u_2
γ : Type ?u.104526
δ : Type ?u.104529
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CompactSpace α
inst✝ : T2Space β
f : α ≃ β
hf : Continuous ↑f
C : Set α
hC : IsClosed C
⊢ IsClosed (↑f.symm ⁻¹' C)
have hC' : IsClosed (f '' C) := (hC.isCompact.image hf).isClosed
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.104526
δ : Type ?u.104529
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : CompactSpace α
inst✝ : T2Space β
f : α ≃ β
hf : Continuous ↑f
C : Set α
hC : IsClosed C
hC' : IsClosed (↑f '' C)
⊢ IsClosed (↑f.symm ⁻¹' C)
rwa [Equiv.image_eq_preimage] at hC'