∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {γ : Type u_8} {δ : Type u_9} (f : β → γ → δ) (s : Set β)
  (t : Set γ) (g : δ → α), ⨅ d ∈ Set.image2 f s t, g d = ⨅ b ∈ s, ⨅ c ∈ t, g (f b c)