α : Type u_1
β : Type u_2
γ : Type ?u.270791
δ : Type ?u.270794
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : ClosedEmbedding f
s : Set α
h : IsClosed (f '' s)
⊢ IsClosed (f ⁻¹' (f '' s))
α : Type u_1
β : Type u_2
γ : Type ?u.270791
δ : Type ?u.270794
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : ClosedEmbedding f
s : Set α
h : IsClosed (f '' s)
⊢ IsClosed s
rw [← preimage_image_eq s hf.inj]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.270791
δ : Type ?u.270794
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
hf : ClosedEmbedding f
s : Set α
h : IsClosed (f '' s)
⊢ IsClosed (f ⁻¹' (f '' s))
exact h.preimage hf.continuous