English
Let α be a complete lattice. If f: β × γ → α and s ⊆ β, t ⊆ γ are sets, then the infimum of f over the rectangular region s × t equals the iterated infimum over a ∈ s and b ∈ t of f(a, b).
Русский
Пусть α — полная решетка. Пусть f: β × γ → α и s ⊆ β, t ⊆ γ. Тогда наименьшее значение f на прямоугольнике s × t равно поэлементному инфимуму по элементам a ∈ s и b ∈ t: inf_{(a,b)∈s×t} f(a,b) = inf_{a∈s} inf_{b∈t} f(a,b).
LaTeX
$$$\\inf_{x \\in s \\times t} f(x) = \\inf_{a \\in s} \\inf_{b \\in t} f(a,b)$$$
Lean4
theorem biInf_prod {f : β × γ → α} {s : Set β} {t : Set γ} : ⨅ x ∈ s ×ˢ t, f x = ⨅ (a ∈ s) (b ∈ t), f (a, b) :=
@biSup_prod αᵒᵈ _ _ _ _ _ _
