no goals
ι : Sort ?u.19236
α : Type u_1
β : Type ?u.19242
X : Type ?u.19245
Y : Type ?u.19248
l₁ l₂ : Filter α
⊢ l₁ ⤳ l₂ ↔ l₁ ≤ l₂
simp only [specializes_iff_closure_subset, Filter.closure_singleton, Ici_subset_Ici]