no goals
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s t : Set α
h₁ : IsClosed s
h₂ : interior t = ∅
x : α
x✝ : x ∈ interior (s ∪ t)
u : Set α
hu₁ : IsOpen u
hu₂ : u ⊆ s ∪ t
hx₁ : x ∈ u
hx₂ : ¬x ∈ s
this : u \ s ⊆ t
⊢ u \ s ⊆ interior t
rwa [(IsOpen.sdiff hu₁ h₁).subset_interior_iff]
no goals
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s t : Set α
h₁ : IsClosed s
h₂ : interior t = ∅
x : α
x✝ : x ∈ interior (s ∪ t)
u : Set α
hu₁ : IsOpen u
hu₂ : u ⊆ s ∪ t
hx₁ : x ∈ u
hx₂ : ¬x ∈ s
this✝ : u \ s ⊆ t
this : u \ s ⊆ interior t
⊢ u \ s ⊆ ∅
rwa [h₂] at this