English
Let α be a distributive lattice with top. For finite s ⊆ ι, t ⊆ κ and f: ι → α, g: κ → α, one has\n\\[ \\left(\\bigwedge_{i∈s} f(i)\\right) \\vee \\left(\\bigwedge_{j∈t} g(j)\\right) = \\bigwedge_{(i,j)∈s×t} \\left( f(i) \\vee g(j) \\right). \\]
Русский
Пусть α — дистрибутивная решётка с верхней границей. Для конечных множеств s ⊆ ι, t ⊆ κ и функций f: ι → α, g: κ → α выполняется\n\\[ \\left(\\bigwedge_{i∈s} f(i)\\right) \\vee \\left(\\bigwedge_{j∈t} g(j)\\right) = \\bigwedge_{(i,j)∈s×t} \\left( f(i) \\vee g(j) \\right). \\]
LaTeX
$$$$ \\left( \\bigwedge_{i \in s} f(i) \\right) \\vee \\left( \\bigwedge_{j \in t} g(j) \\right) = \\bigwedge_{(i,j) \\in s \\times t} \\left( f(i) \\vee g(j) \\right). $$$$
Lean4
theorem inf_sup_inf (s : Finset ι) (t : Finset κ) (f : ι → α) (g : κ → α) :
s.inf f ⊔ t.inf g = (s ×ˢ t).inf fun i => f i.1 ⊔ g i.2 :=
@sup_inf_sup αᵒᵈ _ _ _ _ _ _ _ _
