Theorem: le_generateFrom_iff_subset_isOpen (LeanCourse/Lectures/Lecture7Before.lean)

State before:
n : ℕ
α : Type u_1
t : TopologicalSpace α
g : Set (Set α)
h : g ⊆ {s | IsOpen s}
⊢ {s | IsOpen s} ⊆ {s | IsOpen s}
Tactic:
sorry
State after:
no goals