Theorem: interior_eq_compl_closure_compl (src/Pre.lean)

State before:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ interior s = (closure sᶜ)ᶜ
Tactic:
rw [← compl_compl s, compl_compl sᶜ, interior_compl]
State after:
no goals