α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : NormalSpace α
s t : Set α
hs : IsClosed s
ht : IsOpen t
hst : s ⊆ t
this : Disjoint s (tᶜ)
⊢ ∃ u, IsOpen u ∧ s ⊆ u ∧ closure u ⊆ t
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : NormalSpace α
s t : Set α
hs : IsClosed s
ht : IsOpen t
hst : s ⊆ t
⊢ ∃ u, IsOpen u ∧ s ⊆ u ∧ closure u ⊆ t
have : Disjoint s (tᶜ) := Set.disjoint_left.mpr fun x hxs hxt => hxt (hst hxs)
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : NormalSpace α
s t : Set α
hs : IsClosed s
ht : IsOpen t
hst : s ⊆ t
this : Disjoint s (tᶜ)
s' t' : Set α
hs' : IsOpen s'
ht' : IsOpen t'
hss' : s ⊆ s'
htt' : tᶜ ⊆ t'
hs't' : Disjoint s' t'
⊢ ∃ u, IsOpen u ∧ s ⊆ u ∧ closure u ⊆ t
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : NormalSpace α
s t : Set α
hs : IsClosed s
ht : IsOpen t
hst : s ⊆ t
this : Disjoint s (tᶜ)
⊢ ∃ u, IsOpen u ∧ s ⊆ u ∧ closure u ⊆ t
rcases normal_separation hs (isClosed_compl_iff.2 ht) this with
  ⟨s', t', hs', ht', hss', htt', hs't'⟩
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : NormalSpace α
s t : Set α
hs : IsClosed s
ht : IsOpen t
hst : s ⊆ t
this : Disjoint s (tᶜ)
s' t' : Set α
hs' : IsOpen s'
ht' : IsOpen t'
hss' : s ⊆ s'
htt' : tᶜ ⊆ t'
hs't' : Disjoint s' t'
⊢ s' ⊆ t'ᶜ
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : NormalSpace α
s t : Set α
hs : IsClosed s
ht : IsOpen t
hst : s ⊆ t
this : Disjoint s (tᶜ)
s' t' : Set α
hs' : IsOpen s'
ht' : IsOpen t'
hss' : s ⊆ s'
htt' : tᶜ ⊆ t'
hs't' : Disjoint s' t'
⊢ ∃ u, IsOpen u ∧ s ⊆ u ∧ closure u ⊆ t
refine ⟨s', hs', hss', Subset.trans (closure_minimal ?_ (isClosed_compl_iff.2 ht'))
  (compl_subset_comm.1 htt')⟩
no goals
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : NormalSpace α
s t : Set α
hs : IsClosed s
ht : IsOpen t
hst : s ⊆ t
this : Disjoint s (tᶜ)
s' t' : Set α
hs' : IsOpen s'
ht' : IsOpen t'
hss' : s ⊆ s'
htt' : tᶜ ⊆ t'
hs't' : Disjoint s' t'
⊢ s' ⊆ t'ᶜ
exact fun x hxs hxt => hs't'.le_bot ⟨hxs, hxt⟩