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

State before:
X : Type
F : Set (Set ℝ)
hF : ∀ s ∈ F, IsOpen s
⊢ IsOpen (⋃₀ F)
Tactic:
sorry
State after:
no goals