no goals
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s t : Set α
⊢ closure s \ closure t = closure tᶜ ∩ closure s
simp only [diff_eq, inter_comm]
no goals
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t✝ : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s t : Set α
⊢ closure (closure tᶜ ∩ s) = closure (s \ closure t)
simp only [diff_eq, inter_comm]