English
Let f: β → γ → α, s ⊆ β, t ⊆ γ, and g: δ → α. Then the infimum over image2 f s t of g equals the iterated infimum over b ∈ s and c ∈ t of g(f b c).
Русский
Пусть f: β → γ → α, s ⊆ β, t ⊆ γ, и g: δ → α. Тогда инфимуум над образованием image2 f над s×t удовлетворяет: inf_{d ∈ image2 f s t} g(d) = inf_{b ∈ s} inf_{c ∈ t} g(f(b,c)).
LaTeX
$$$\\inf_{d \\in \\mathrm{image2}\\,f\\,s\\,t} g(d) = \\inf_{b \\in s} \\inf_{c \\in t} g(f(b,c))$$$
Lean4
theorem iInf_image2 {γ δ} (f : β → γ → δ) (s : Set β) (t : Set γ) (g : δ → α) :
⨅ d ∈ image2 f s t, g d = ⨅ b ∈ s, ⨅ c ∈ t, g (f b c) :=
iSup_image2 f s t (toDual ∘ g)