exists_ne_one_of_finprod_mem_ne_one

English

If the finprod is not equal to 1, there exists x ∈ s with f(x) ≠ 1.

Русский

Если финпроизводство не равно 1, существует x∈s такое, что f(x) ≠ 1.

LaTeX

$$$\\displaystyle (\\prodᶠ i ∈ s, f i) ≠ 1 \\Rightarrow ∃ x ∈ s, f x ≠ 1$$$

Lean4

/-- If the product of `f i` over `i ∈ s` is not equal to `1`, then there is some `x ∈ s` such that
`f x ≠ 1`. -/
@[to_additive /-- If the sum of `f i` over `i ∈ s` is not equal to `0`, then there is some `x ∈ s`
          such that `f x ≠ 0`. -/
    ]
theorem exists_ne_one_of_finprod_mem_ne_one (h : ∏ᶠ i ∈ s, f i ≠ 1) : ∃ x ∈ s, f x ≠ 1 :=
  by
  by_contra! h'
  exact h (finprod_mem_of_eqOn_one h')

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