α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ frontier (sᶜ) = closure (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_compl, ← closure_compl]
no goals
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ frontier (sᶜ) = closure (sᶜ) ∩ interior (sᶜ)ᶜ
rfl