sorry_proof
R : Type ?u.1691
inst✝⁷ : RealScalar R
W : Type ?u.1697
inst✝⁶ : SemiHilbert R W
X✝ : Type ?u.1724
inst✝⁵ : SemiHilbert R X✝
Y : Type ?u.1745
inst✝⁴ : SemiHilbert R Y
inst✝³ : Module ℝ Y
Z : Type ?u.2563
inst✝² : SemiHilbert R Z
inst✝¹ : Module ℝ Z
X : Type u_1
inst✝ : TopologicalSpace X
A B : Set X
hA : IsClosed A
hB : IsClosed B
⊢ frontier (A ∩ B) = frontier A ∩ B ∪ frontier B ∩ A
no goals