prod_lt_one_iff_of_le_one — Mathlib

English

If f(i) ≤ 1 for all i ∈ s, then 1 < ∏_{i∈s} f(i) if and only if there exists i ∈ s with f(i) > 1.

Русский

Если для всех i ∈ s верно f(i) ≤ 1, тогда 1 < ∏_{i∈s} f(i) тогда и только тогда существует i ∈ s такое, что f(i) > 1.

LaTeX

$$$ \\forall \\iota\\, N\\, [\\text{MulLeftMono } N], ( \\forall i \\in s, f(i) \\le 1 ) \\Rightarrow \\left( \\left( \\prod_{i \\in s} f(i) \\right) < 1 \\iff \\exists i \\in s, 1 < f(i) \\right). $$$

Lean4

@[to_additive]
theorem prod_lt_one_iff_of_le_one [MulLeftMono N] (hf : ∀ x ∈ s, f x ≤ 1) : ∏ x ∈ s, f x < 1 ↔ ∃ x ∈ s, f x < 1 :=
  one_lt_prod_iff_of_one_le (N := Nᵒᵈ) hf

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