inf'_mul_le_mul_inf'_of_nonneg — Mathlib

English

Under nonnegativity, the infimum of the product dominates the product of infima: inf'_hs a · inf'_hs b ≤ inf'_hs (a b).

Русский

При неотрицательности имеет место: inf'_hs a · inf'_hs b ≤ inf'_hs (a b).

LaTeX

$$$\inf'_{i\in s} a_i \cdot \inf'_{i\in s} b_i \le \inf'_{i\in s} (a_i b_i).$$$

Lean4

theorem inf'_mul_le_mul_inf'_of_nonneg [SemilatticeInf M₀] [PosMulMono M₀] [MulPosMono M₀] (ha : ∀ i ∈ s, 0 ≤ a i)
    (hb : ∀ i ∈ s, 0 ≤ b i) (hs) : s.inf' hs a * s.inf' hs b ≤ s.inf' hs (a * b) :=
  le_inf' _ _ fun _i hi ↦ mul_le_mul (inf'_le _ hi) (inf'_le _ hi) (le_inf' _ _ hb) (ha _ hi)

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