le_iInf₂_mul — Mathlib

English

The inequality dually mirrors iSup_mul_le: the product of infima is bounded above by the infimum of products, in a dual lattice.

Русский

Дуально зеркально iSup_mul_le: произведение инфимума не превосходит инфимум произведений, в двойственной структуре.

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 : ι) → κ i → α) : (⨅ (i) (j), u i j) * ⨅ (i) (j), v i j ≤ ⨅ (i) (j), u i j * v i j :=
  iSup₂_mul_le (α := αᵒᵈ) ..

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