no goals
α : Type u
t : TopologicalSpace α
b : Set (Set α)
hb : IsTopologicalBasis b
s : Set α
a : α
⊢ (∀ (i : Set α), i ∈ b ∧ a ∈ i → Set.Nonempty (i ∩ s)) ↔ ∀ (o : Set α), o ∈ b → a ∈ o → Set.Nonempty (o ∩ s)
simp only [and_imp]