single_lt_prod' — Mathlib

English

If i ≠ j and i,j ∈ s, with f(j) > 1 and f(k) ≥ 1 for all k ∈ s, then f(i) < ∏_{k∈s} f(k).

Русский

Если элементы i и j принадлежат s, i ≠ j, f(j) > 1 и для каждого k ∈ s верно f(k) ≥ 1, тогда f(i) < произведение по всем k ∈ s.

LaTeX

$$$i,j ∈ s,\\ i ≠ j,\\ f(j) > 1,\\ ∀k∈s, k ≠ i \\Rightarrow 1 ≤ f(k)\\;\\Rightarrow \\; f(i) < \\prod_{k∈s} f(k)$$$

Lean4

@[to_additive single_lt_sum]
theorem single_lt_prod' {i j : ι} (hij : j ≠ i) (hi : i ∈ s) (hj : j ∈ s) (hlt : 1 < f j)
    (hle : ∀ k ∈ s, k ≠ i → 1 ≤ f k) : f i < ∏ k ∈ s, f k :=
  calc
    f i = ∏ k ∈ { i }, f k := by rw [prod_singleton]
    _ < ∏ k ∈ s, f k :=
      prod_lt_prod_of_subset' (singleton_subset_iff.2 hi) hj (mt mem_singleton.1 hij) hlt fun k hks hki ↦
        hle k hks (mt mem_singleton.2 hki)

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