English
Let s ⊆ α and t ⊆ β be finite, and g: γ → δ. If image₂ f s t is nonempty, then the infimum of g over the set image₂ f s t equals the iterated infimum: inf over x in s of inf over y in t of g(f(x,y)).
Русский
Пусть s ⊆ α и t ⊆ β — конечные множества, и g: γ → δ. Если image₂ f s t не пусто, то нижний предел функции g на множестве image₂ f s t равен повторному нижнему пределу: inf_{x∈s} inf_{y∈t} g(f(x,y)).
LaTeX
$$$\displaystyle \text{If }(\operatorname{image}_2 f nobreak s t)\neq\varnothing,\; \inf'\big(\operatorname{image}_2 f s t\big)\; g = \inf'\!\; s\; (\mathrm{inf}'\; t\; (g\circ f))$$$
Lean4
theorem inf'_image₂_left (g : γ → δ) (h : (image₂ f s t).Nonempty) :
inf' (image₂ f s t) h g = inf' s h.of_image₂_left fun x ↦ inf' t h.of_image₂_right (g <| f x ·) :=
sup'_image₂_left (δ := δᵒᵈ) g h
