no goals
α : Type u
β : Type v
ι : Sort w
a✝ : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝² : TopologicalSpace α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
⊢ (∀ (ib : Set α), a ∈ ib ∧ IsOpen ib → ∃ ia, True ∧ ∀ (x : β), x ∈ Ici ia → f x ∈ ib) ↔
    ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : β), N ≤ n → f n ∈ U
simp only [and_imp, exists_prop, true_and_iff, mem_Ici, ge_iff_le]