∀ {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Finite ι] [inst : Preorder ι'] [Nonempty ι'] [IsDirectedOrder ι']
  [inst_3 : Order.Coframe α] {f : ι → ι' → α}, (∀ (i : ι), Antitone (f i)) → ⨅ j, ⨆ i, f i j = ⨆ i, ⨅ j, f i j