no goals
ι : Sort u_2
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s : Set α
h : Directed (fun x x_1 => x ≤ x_1) f
⊢ Disjoint a (⨆ (i : ι), f i) ↔ ∀ (i : ι), Disjoint a (f i)
simp_rw [disjoint_iff, h.inf_iSup_eq, iSup_eq_bot]