no goals
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort u_1
inst✝ : Frame α
s t : Set α
a b : α
f : (i : ι) → κ i → α
⊢ Disjoint a (⨆ (i : ι) (j : κ i), f i j) ↔ ∀ (i : ι) (j : κ i), Disjoint a (f i j)
simp_rw [disjoint_iSup_iff]