∀ {α : Type u_1} {β : Type u_2} [inst : CompletelyDistribLattice α] [inst_1 : CompletelyDistribLattice β]
  {ι : Type (max u_1 u_2)} {κ : ι → Type (max u_1 u_2)} (f : (a : ι) → κ a → α × β),
  ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)