prod_lt_prod_of_nonempty — Mathlib

English

If s is nonempty and there exists i ∈ s with f(i) < g(i) and f(i) > 0, then ∏ f(i) < ∏ g(i).

Русский

Если множество s непусто и существует i∈s с f(i) < g(i) и f(i) > 0, то произведение f(i) по s меньше произведения g(i) по s.

LaTeX

$$$$s\\ \\text{nonempty} \\quad \\Rightarrow \\quad \\exists i \\in s, f(i) < g(i) \\Rightarrow \\prod_{i \\in s} f(i) < \\prod_{i \in s} g(i).$$$$

Lean4

theorem prod_lt_prod_of_nonempty (hf : ∀ i ∈ s, 0 < f i) (hfg : ∀ i ∈ s, f i < g i) (h_ne : s.Nonempty) :
    ∏ i ∈ s, f i < ∏ i ∈ s, g i :=
  by
  apply prod_lt_prod hf fun i hi => le_of_lt (hfg i hi)
  obtain ⟨i, hi⟩ := h_ne
  exact ⟨i, hi, hfg i hi⟩

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