α : Type u_1
β : Type u_2
γ : Type ?u.257906
δ : Type ?u.257909
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h₁ : Continuous f
h₂ : Injective f
h₃ : IsOpenMap f
⊢ ∀ (a : α), 𝓝 a = comap f (𝓝 (f a))
α : Type u_1
β : Type u_2
γ : Type ?u.257906
δ : Type ?u.257909
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h₁ : Continuous f
h₂ : Injective f
h₃ : IsOpenMap f
⊢ OpenEmbedding f
simp only [openEmbedding_iff_embedding_open, embedding_iff, inducing_iff_nhds, *, and_true_iff]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.257906
δ : Type ?u.257909
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α → β
h₁ : Continuous f
h₂ : Injective f
h₃ : IsOpenMap f
⊢ ∀ (a : α), 𝓝 a = comap f (𝓝 (f a))
exact fun a =>
  le_antisymm (h₁.tendsto _).le_comap (@comap_map _ _ (𝓝 a) _ h₂ ▸ comap_mono (h₃.nhds_le _))