α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NormalSpace β
f : α → β
hf : ClosedEmbedding f
s t : Set α
hs : IsClosed s
ht : IsClosed t
hst : Disjoint s t
H : SeparatedNhds (f '' s) (f '' t)
⊢ SeparatedNhds s t
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NormalSpace β
f : α → β
hf : ClosedEmbedding f
s t : Set α
hs : IsClosed s
ht : IsClosed t
hst : Disjoint s t
⊢ SeparatedNhds s t
have H : SeparatedNhds (f '' s) (f '' t) :=
  NormalSpace.normal (f '' s) (f '' t) (hf.isClosedMap s hs) (hf.isClosedMap t ht)
    (disjoint_image_of_injective hf.inj hst)
no goals
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NormalSpace β
f : α → β
hf : ClosedEmbedding f
s t : Set α
hs : IsClosed s
ht : IsClosed t
hst : Disjoint s t
H : SeparatedNhds (f '' s) (f '' t)
⊢ SeparatedNhds s t
exact (H.preimage hf.continuous).mono (subset_preimage_image _ _) (subset_preimage_image _ _)