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 = s^{\\inf} h.fst (\\lambda i, t^{\\inf} h.snd (\\lambda j, f(i,j))). \\]
Русский
Пусть α — полулогическая решётка с inf. Тогда для конечных s ⊆ β, t ⊆ γ и h ≠ ∅ выполняется\n\\[ (s × t)^{\\inf} h f = s^{\\inf} h.fst (λ i, t^{\\inf} h.snd (λ j, f(i,j))). \\]
LaTeX
$$$$ (s \\times t)^{\\inf} h f = s^{\\inf} h.fst \\; (\\lambda i \\mapsto t^{\\inf} h.snd \\; (\\lambda j \\mapsto f(i,j))). $$$$
Lean4
theorem inf'_product_left {t : Finset γ} (h : (s ×ˢ t).Nonempty) (f : β × γ → α) :
(s ×ˢ t).inf' h f = s.inf' h.fst fun i => t.inf' h.snd fun i' => f ⟨i, i'⟩ :=
sup'_product_left (α := αᵒᵈ) h f
