one_lt_prod_iff_of_one_le — Mathlib

English

Assume f(i) ≥ 1 for i ∈ s. Then 1 < ∏_{i∈s} f(i) if and only if there exists i ∈ s with f(i) > 1.

Русский

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

LaTeX

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

Lean4

@[to_additive sum_pos_iff_of_nonneg]
theorem one_lt_prod_iff_of_one_le [MulLeftMono N] (hf : ∀ x ∈ s, 1 ≤ f x) : 1 < ∏ x ∈ s, f x ↔ ∃ x ∈ s, 1 < f x :=
  by
  have hsum : 1 ≤ ∏ x ∈ s, f x := one_le_prod' hf
  rw [hsum.lt_iff_ne', Ne, prod_eq_one_iff_of_one_le' hf, not_forall]
  simp +contextual [← exists_prop, -exists_const_iff, hf _ _ |>.lt_iff_ne']

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