no goals
ι : Sort ?u.15646
α : Type u_1
β : Type ?u.15652
X : Type ?u.15655
Y : Type ?u.15658
s : Set (Filter α)
l : Filter α
⊢ l ∈ interior s ↔ ∃ t, t ∈ l ∧ Iic (𝓟 t) ⊆ s
rw [mem_interior_iff_mem_nhds, mem_nhds_iff]