Theorem: SciLean.frontier_inter (SciLean/Core/Integral/Frontier.lean)

State before:
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
Tactic:
sorry_proof
State after:
no goals