prod_eq_one_iff_of_le_one' — Mathlib

English

If f(i) ≤ 1 for all i ∈ s, then ∏_{i∈s} f(i) = 1 if and only if f(i) = 1 for all i ∈ s.

Русский

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

LaTeX

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

Lean4

@[to_additive sum_eq_zero_iff_of_nonpos]
theorem prod_eq_one_iff_of_le_one' [MulLeftMono N] : (∀ i ∈ s, f i ≤ 1) → ((∏ i ∈ s, f i) = 1 ↔ ∀ i ∈ s, f i = 1) :=
  prod_eq_one_iff_of_one_le' (N := Nᵒᵈ)

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