α : Type u
t : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set α
ou : IsOpen u
⊢ u = ⋃₀ {s | s ∈ B ∧ s ⊆ u}
α : Type u
t : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set α
ou : IsOpen u
⊢ u = ⋃ (i : ↑{s | s ∈ B ∧ s ⊆ u}), ↑i
rw [← sUnion_eq_iUnion]
no goals
α : Type u
t : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set α
ou : IsOpen u
⊢ u = ⋃₀ {s | s ∈ B ∧ s ⊆ u}
apply hB.open_eq_sUnion' ou