nonempty_of_finprod_mem_ne_one — Mathlib

English

If the finite product ∏_{i∈s} f(i) ≠ 1, then s is nonempty.

Русский

Если конечное произведение ∏_{i∈s} f(i) не равно 1, то множество s непусто.

LaTeX

$$\left(\prod_{i \in s} f(i)\right) \neq 1 \Rightarrow s \neq \emptyset$$

Lean4

/-- A set `s` is nonempty if the product of some function over `s` is not equal to `1`. -/
@[to_additive /-- A set `s` is nonempty if the sum of some function over `s` is not equal to `0`. -/
    ]
theorem nonempty_of_finprod_mem_ne_one (h : ∏ᶠ i ∈ s, f i ≠ 1) : s.Nonempty :=
  nonempty_iff_ne_empty.2 fun h' => h <| h'.symm ▸ finprod_mem_empty

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