no goals
ι : Sort ?u.99428
α : Type u_1
inst✝² : CompleteLattice α
f : ι → α
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
a b : α
s : Set α
h : DirectedOn (fun x x_1 => x ≤ x_1) s
⊢ Disjoint (sSup s) a ↔ ∀ ⦃b : α⦄, b ∈ s → Disjoint b a
simp_rw [disjoint_iff, h.sSup_inf_eq, iSup_eq_bot]