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