English
Let α be a semilattice with supremum. For finite s ⊆ β, t ⊆ γ and h : (s × t) ≠ ∅, with f : β × γ → α, we have\n\\[ (s × t)^{\\inf} h f = t^{\\inf} h.snd (\\lambda i', s^{\\inf} h.fst (\\lambda i, f(i,i')). \\]
Русский
Пусть α обладает наибольшей верхней границей. Для конечных s ⊆ β, t ⊆ γ и h ≠ ∅ с f : β × γ → α выполняется\n\\[ (s × t)^{\\inf} h f = t^{\\inf} h.snd (λ i', s^{\\inf} h.fst (λ i, f(i,i'))). \\]
LaTeX
$$$$ (s \\times t)^{\\inf} h f = t^{\\inf} h.snd \\; (\\lambda i' \\mapsto s^{\\inf} h.fst \\; (\\lambda i \\mapsto f(i,i')).) $$$$
Lean4
theorem sup'_product_right {t : Finset γ} (h : (s ×ˢ t).Nonempty) (f : β × γ → α) :
(s ×ˢ t).sup' h f = t.sup' h.snd fun i' => s.sup' h.fst fun i => f ⟨i, i'⟩ := by
rw [sup'_product_left, Finset.sup'_comm]
