English
Let f: β → γ → α, s ⊆ β, t ⊆ γ, and g: δ → α. Then the supremum over the image2 f s t of g is equal to the iterated supremum over b ∈ s and c ∈ t of g(f b c).
Русский
Пусть f: β → γ → α, s ⊆ β, t ⊆ γ, и g: δ → α. Тогда наибольшие значения по образу f над s×t равны по порядку через b ∈ s и c ∈ t: sup_{d ∈ image2 f s t} g(d) = sup_{b ∈ s} sup_{c ∈ t} g(f(b,c)).
LaTeX
$$$\\sup_{d \\in \\mathrm{image2}\\,f\\,s\\,t} g(d) = \\sup_{b \\in s} \\sup_{c \\in t} g(f(b,c))$$$
Lean4
theorem iSup_image2 {γ δ} (f : β → γ → δ) (s : Set β) (t : Set γ) (g : δ → α) :
⨆ d ∈ image2 f s t, g d = ⨆ b ∈ s, ⨆ c ∈ t, g (f b c) := by rw [← image_prod, iSup_image, biSup_prod]
