English
Let α be a ConditionallyCompleteLattice with a multiplication that is monotone in both arguments. For f,g : I → α bounded below, the product of their infima is a lower bound for the infimum of the pairwise products: (inf_i f(i))·(inf_i g(i)) ≤ inf_i (f(i)·g(i)).
Русский
Пусть α — условно завершённая решётка с умножением, монотонным по каждому аргументу. Для f,g : I → α с нижними ограничениями выполняется неравенство: (inf_i f(i))·(inf_i g(i)) ≤ inf_i (f(i)·g(i)).
LaTeX
$$$\displaystyle \Bigl(\inf_i f(i)\Bigr) \cdot \Bigl(\inf_i g(i)\Bigr) \le \inf_i \bigl( f(i) \cdot g(i) \bigr)$$$
Lean4
@[to_additive]
theorem ciInf_mul_ciInf_le_ciInf_mul [MulLeftMono α] [MulRightMono α] {f g : ι → α} (hf : BddBelow (range f))
(hg : BddBelow (range g)) : (⨅ i, f i) * ⨅ i, g i ≤ ⨅ i, f i * g i :=
le_ciInf fun i ↦ mul_le_mul' (ciInf_le hf i) (ciInf_le hg i)
