English
Let α be a distributive lattice with bottom. For any finite sets s ⊆ ι, t ⊆ κ and functions f: ι → α, g: κ → α, one has\n\\[ \\left(\\bigvee_{i∈s} f(i)\\right) \\wedge \\left(\\bigvee_{j∈t} g(j)\\right) = \\bigvee_{(i,j)∈s×t} \\left(f(i) \\wedge g(j)\\right). \\]
Русский
Пусть α — распределённая решётка с нулём. Для любых конечных множеств s ⊆ ι, t ⊆ κ и функций f: ι → α, g: κ → α верно\n[максимум по s] f ∧ [максимум по t] g = [максимум по произведению] (i,j)∈s×t: f(i) ∧ g(j).
LaTeX
$$$$ \\left( \\bigvee_{i \\in s} f(i) \\right) \\wedge \\left( \\bigvee_{j \\in t} g(j) \\right) = \\bigvee_{(i,j) \\in s \\times t} \\left( f(i) \\wedge g(j) \\right). $$$$
Lean4
theorem sup_inf_sup (s : Finset ι) (t : Finset κ) (f : ι → α) (g : κ → α) :
s.sup f ⊓ t.sup g = (s ×ˢ t).sup fun i => f i.1 ⊓ g i.2 := by
simp_rw [Finset.sup_inf_distrib_right, Finset.sup_inf_distrib_left, sup_product_left]
