exists_ne_one_of_prod_ne_one — Mathlib

English

If ∏_{x∈s} f x ≠ 1, then there exists a ∈ s with f a ≠ 1.

Русский

Если произведение по s не равно единице, то найдётся элемент a ∈ s такой, что f a ≠ 1.

LaTeX

$$$\left(\prod x \in s, f x\right) \neq 1 \implies \exists a \in s, f a \neq 1$$$

Lean4

@[to_additive]
theorem exists_ne_one_of_prod_ne_one (h : ∏ x ∈ s, f x ≠ 1) : ∃ a ∈ s, f a ≠ 1 := by
  classical
  rw [← prod_filter_ne_one] at h
  rcases nonempty_of_prod_ne_one h with ⟨x, hx⟩
  exact ⟨x, (mem_filter.1 hx).1, by simpa using (mem_filter.1 hx).2⟩

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