no goals
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort ?u.7410
inst✝ : Frame α
s t : Set α
a b : α
f : ι → α
⊢ Disjoint (⨆ (i : ι), f i) a ↔ ∀ (i : ι), Disjoint (f i) a
simp only [disjoint_iff, iSup_inf_eq, iSup_eq_bot]