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

State before:
R : Type u_2
inst✝⁷ : RealScalar R
W : Type ?u.3766
inst✝⁶ : SemiHilbert R W
X✝ : Type ?u.3793
inst✝⁵ : SemiHilbert R X✝
Y : Type ?u.3814
inst✝⁴ : SemiHilbert R Y
inst✝³ : Module ℝ Y
Z : Type ?u.4632
inst✝² : SemiHilbert R Z
inst✝¹ : Module ℝ Z
X : Type u_1
inst✝ : TopologicalSpace X
φ ψ : X → R
⊢ frontier {x | φ x ≤ ψ x} = {x | φ x = ψ x}
Tactic:
sorry_proof
State after:
no goals