prod_lt_one' — Mathlib

English

Let s be a finite index set and f: s → M. If every value f(i) is ≤ 1 and at least one value is strictly less than 1, then the product ∏_{i∈s} f(i) is strictly less than 1.

Русский

Пусть s — конечное множество индексов и функция f: s → M. Если для каждого i ∈ s выполняется f(i) ≤ 1 и существует i0 ∈ s such that f(i0) < 1, тогда произведение ∏_{i∈s} f(i)strictly меньше 1.

LaTeX

$$$\left( \forall i \in s,\ f(i) \le 1 \right) \land \left( \exists i \in s,\ f(i) < 1 \right) \implies \left( \prod_{i \in s} f(i) < 1 \right)$$$

Lean4

@[to_additive]
theorem prod_lt_one' (h : ∀ i ∈ s, f i ≤ 1) (hs : ∃ i ∈ s, f i < 1) : ∏ i ∈ s, f i < 1 :=
  prod_const_one.le.trans_lt' <| prod_lt_prod' h hs

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