English
Let α be a ConditionallyCompleteLattice equipped with a multiplication that is monotone in both arguments. If f and g are indexable families taking values in α and are bounded above, then the supremum of the pointwise products is bounded above by the product of the supremums: ⨆ i, f(i)·g(i) ≤ (⨆ i, f(i))·(⨆ i, g(i)).
Русский
Пусть α — частично упорядоченное решёточное множество с умножением, монотонным по каждому аргументу. Пусть f, g : I → α таковы, что диапазоны ограничены сверху. Тогда верхняя грань по точечным произведениям не превосходит произведения верхних граней: ⨆ i, f(i)·g(i) ≤ (⨆ i, f(i))·(⨆ i, g(i)).
LaTeX
$$$\displaystyle \bigvee_i \bigl( f(i) \cdot g(i) \bigr) \le \Bigl(\bigvee_i f(i)\Bigr) \cdot \Bigl(\bigvee_i g(i)\Bigr)$$$
Lean4
@[to_additive]
theorem ciSup_mul_le_ciSup_mul_ciSup [MulLeftMono α] [MulRightMono α] {f g : ι → α} (hf : BddAbove (range f))
(hg : BddAbove (range g)) : ⨆ i, f i * g i ≤ (⨆ i, f i) * ⨆ i, g i :=
ciSup_le fun i ↦ mul_le_mul' (le_ciSup hf i) (le_ciSup hg i)
