le_iInf_mul — Mathlib

English

In a complete lattice with multiplication that is monotone in both arguments, the product of the infima is less than or equal to the infimum of the pointwise products.

Русский

В полной решетке с монотонной по обе стороны умножения неравенство: (inf_i u_i) (inf_i v_i) ≤ inf_i (u_i v_i).

LaTeX

$$$$ \\left( \\inf_{i} u(i) \\right) \\cdot \\left( \\inf_{i} v(i) \\right) \\le \\inf_{i} \\left( u(i) \\cdot v(i) \\right) $$$$

Lean4

@[to_additive]
theorem le_iInf_mul (u v : ι → α) : (⨅ i, u i) * ⨅ i, v i ≤ ⨅ i, u i * v i :=
  iSup_mul_le (α := αᵒᵈ) ..

Похожие утверждения