English
Let α be a semilattice with infimum. 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'))). \\]
Русский
Пусть α — полулогическая решётка с inf. Тогда для конечных s ⊆ β, t ⊆ γ и h ≠ ∅ выполняется\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 inf'_product_right {t : Finset γ} (h : (s ×ˢ t).Nonempty) (f : β × γ → α) :
(s ×ˢ t).inf' h f = t.inf' h.snd fun i' => s.inf' h.fst fun i => f ⟨i, i'⟩ :=
sup'_product_right (α := αᵒᵈ) h f
