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

State before:
X : Type
⊢ IsOpen Set.univ
Tactic:
sorry
State after:
no goals