Theorem: Section10sheet1.Real.isOpen_inter (FormalisingMathematics2024/Section10TopologicalSpaces/Sheet1.lean)

State before:
X : Type
s t : Set ℝ
hs : IsOpen s
ht : IsOpen t
⊢ IsOpen (s ∩ t)
Tactic:
sorry
State after:
no goals