mul_inf_le_inf_mul_of_nonneg — Mathlib

English

Under similar nonnegativity assumptions, the product of infima is bounded by the infimum of the pairwise product: (inf_i a_i)(inf_i b_i) ≤ inf_i (a_i b_i).

Русский

При тех же предположениях неотрицательности имеем: (inf_i a_i)(inf_i b_i) ≤ inf_i (a_i b_i).

LaTeX

$$$\left(\inf_{i\in s} a_i\right)\left(\inf_{i\in s} b_i\right) \le \inf_{i\in s} (a_i b_i).$$$

Lean4

theorem mul_inf_le_inf_mul_of_nonneg [SemilatticeInf M₀] [OrderTop M₀] [PosMulMono M₀] [MulPosMono M₀]
    (ha : ∀ i ∈ s, 0 ≤ a i) (hb : ∀ i ∈ s, 0 ≤ b i) : s.inf a * s.inf b ≤ s.inf (a * b) :=
  Finset.le_inf fun i hi ↦ mul_le_mul (inf_le hi) (inf_le hi) (Finset.le_inf hb) (ha i hi)

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