α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ (interior sᶜ ∩ interior (sᶜ)ᶜ)ᶜ = interior s ∪ interior (sᶜ)
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ frontier sᶜ = interior s ∪ interior (sᶜ)
rw [frontier_eq_inter_compl_interior]
no goals
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ (interior sᶜ ∩ interior (sᶜ)ᶜ)ᶜ = interior s ∪ interior (sᶜ)
simp only [compl_inter, compl_compl]