α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T5Space β
e : α → β
he : _root_.Embedding e
this : T1Space α
⊢ T5Space α
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T5Space β
e : α → β
he : _root_.Embedding e
⊢ T5Space α
haveI := he.t1Space
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T5Space β
e : α → β
he : _root_.Embedding e
this : T1Space α
s t : Set α
hd₁ : Disjoint (closure s) t
hd₂ : Disjoint s (closure t)
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T5Space β
e : α → β
he : _root_.Embedding e
this : T1Space α
⊢ T5Space α
refine' ⟨fun s t hd₁ hd₂ => _⟩
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T5Space β
e : α → β
he : _root_.Embedding e
this : T1Space α
s t : Set α
hd₁ : Disjoint (closure s) t
hd₂ : Disjoint s (closure t)
⊢ Disjoint (comap e (𝓝ˢ (e '' s))) (comap e (𝓝ˢ (e '' t)))
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T5Space β
e : α → β
he : _root_.Embedding e
this : T1Space α
s t : Set α
hd₁ : Disjoint (closure s) t
hd₂ : Disjoint s (closure t)
⊢ Disjoint (𝓝ˢ s) (𝓝ˢ t)
simp only [he.toInducing.nhdsSet_eq_comap]
case refine_1
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T5Space β
e : α → β
he : _root_.Embedding e
this : T1Space α
s t : Set α
hd₁ : Disjoint (closure s) t
hd₂ : Disjoint s (closure t)
⊢ Disjoint (closure (e '' s)) (e '' t)

case refine_2
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T5Space β
e : α → β
he : _root_.Embedding e
this : T1Space α
s t : Set α
hd₁ : Disjoint (closure s) t
hd₂ : Disjoint s (closure t)
⊢ Disjoint (e '' s) (closure (e '' t))
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T5Space β
e : α → β
he : _root_.Embedding e
this : T1Space α
s t : Set α
hd₁ : Disjoint (closure s) t
hd₂ : Disjoint s (closure t)
⊢ Disjoint (comap e (𝓝ˢ (e '' s))) (comap e (𝓝ˢ (e '' t)))
refine disjoint_comap (completely_normal ?_ ?_)
no goals
case refine_1
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T5Space β
e : α → β
he : _root_.Embedding e
this : T1Space α
s t : Set α
hd₁ : Disjoint (closure s) t
hd₂ : Disjoint s (closure t)
⊢ Disjoint (closure (e '' s)) (e '' t)
rwa [← subset_compl_iff_disjoint_left, image_subset_iff, preimage_compl,
  ← he.closure_eq_preimage_closure_image, subset_compl_iff_disjoint_left]
no goals
case refine_2
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T5Space β
e : α → β
he : _root_.Embedding e
this : T1Space α
s t : Set α
hd₁ : Disjoint (closure s) t
hd₂ : Disjoint s (closure t)
⊢ Disjoint (e '' s) (closure (e '' t))
rwa [← subset_compl_iff_disjoint_right, image_subset_iff, preimage_compl,
  ← he.closure_eq_preimage_closure_image, subset_compl_iff_disjoint_right]