prod_lt_prod' — Mathlib

English

If s is nonempty and for all i ∈ s we have f(i) ≤ g(i), and there exists an i with f(i) < g(i), then ∏_{i∈s} f(i) < ∏_{i∈s} g(i).

Русский

Если s непусто, и для всех i ∈ s верно f(i) ≤ g(i) с существованием элемента i, для которого <, тогда ∏ f(i) < ∏ g(i).

LaTeX

$$$s \\neq \\emptyset \\land (\\forall i \\in s, f(i) ≤ g(i)) \\land (\\exists i \\in s, f(i) < g(i)) \\Rightarrow \\prod_{i \\in s} f(i) < \\prod_{i \\in s} g(i)$$$

Lean4

@[to_additive sum_lt_sum]
theorem prod_lt_prod' (hle : ∀ i ∈ s, f i ≤ g i) (hlt : ∃ i ∈ s, f i < g i) : ∏ i ∈ s, f i < ∏ i ∈ s, g i :=
  Multiset.prod_lt_prod' hle hlt

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