α : Type u_1
β : Type u_2
γ : Type ?u.280474
δ : Type ?u.280477
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h₁ : Continuous f
h₂ : Injective f
h₃ : IsClosedMap f
⊢ inst✝² = induced f inst✝¹
α : Type u_1
β : Type u_2
γ : Type ?u.280474
δ : Type ?u.280477
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h₁ : Continuous f
h₂ : Injective f
h₃ : IsClosedMap f
⊢ ClosedEmbedding f
refine closedEmbedding_of_embedding_closed ⟨⟨?_⟩, h₂⟩ h₃
α : Type u_1
β : Type u_2
γ : Type ?u.280474
δ : Type ?u.280477
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h₁ : Continuous f
h₂ : Injective f
h₃ : IsClosedMap f
s : Set α
hs : IsOpen s
⊢ IsOpen s
α : Type u_1
β : Type u_2
γ : Type ?u.280474
δ : Type ?u.280477
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h₁ : Continuous f
h₂ : Injective f
h₃ : IsClosedMap f
⊢ inst✝² = induced f inst✝¹
refine h₁.le_induced.antisymm fun s hs => ?_
α : Type u_1
β : Type u_2
γ : Type ?u.280474
δ : Type ?u.280477
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h₁ : Continuous f
h₂ : Injective f
h₃ : IsClosedMap f
s : Set α
hs : IsOpen s
⊢ f ⁻¹' (f '' sᶜ)ᶜ = s
α : Type u_1
β : Type u_2
γ : Type ?u.280474
δ : Type ?u.280477
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h₁ : Continuous f
h₂ : Injective f
h₃ : IsClosedMap f
s : Set α
hs : IsOpen s
⊢ IsOpen s
refine ⟨(f '' sᶜ)ᶜ, (h₃ _ hs.isClosed_compl).isOpen_compl, ?_⟩
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.280474
δ : Type ?u.280477
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h₁ : Continuous f
h₂ : Injective f
h₃ : IsClosedMap f
s : Set α
hs : IsOpen s
⊢ f ⁻¹' (f '' sᶜ)ᶜ = s
rw [preimage_compl, preimage_image_eq _ h₂, compl_compl]