English
If the finite set on the left is nonempty, the supremum over image₂ f s t equals the iterated supremum: sup' (image₂ f s t) h g = sup' s h.of_image₂_left (fun x => sup' t h.of_image₂_right (g (f x ·))).
Русский
Если \( (image₂ f s t).Nonempty \), то sup' (image₂ f s t) = sup' s ...
LaTeX
$$$\\forall s:\\ Finset, t:\\ Finset, (image_2 f s t).Nonempty \\Rightarrow sup' (image_2 f s t) h g = sup' s h.of_image_2_left (\\lambda x, sup' t h.of_image_2_right (g \\lvert f x \\cdot\\rangle))$$$
Lean4
theorem sup'_image₂_left (g : γ → δ) (h : (image₂ f s t).Nonempty) :
sup' (image₂ f s t) h g = sup' s h.of_image₂_left fun x ↦ sup' t h.of_image₂_right (g <| f x ·) := by
simp only [image₂, sup'_image, sup'_product_left]; rfl
