exists_one_lt_of_prod_one_of_exists_ne_one'

English

If the product over s of f equals 1 and there exists i ∈ s with f(i) ≠ 1, then there exists i ∈ s with 1 < f(i).

Русский

Если произведение по s равно 1 и существует i ∈ s такое что f(i) ≠ 1, то найдётся i ∈ s с 1 < f(i).

LaTeX

$$$\left( \prod_{i\in s} f(i) = 1 \right) \land \left( \exists i \in s,\ f(i) \neq 1 \right) \implies \left( \exists i \in s,\ 1 < f(i) \right)$$$

Lean4

@[to_additive exists_pos_of_sum_zero_of_exists_nonzero]
theorem exists_one_lt_of_prod_one_of_exists_ne_one' (f : ι → M) (h₁ : ∏ i ∈ s, f i = 1) (h₂ : ∃ i ∈ s, f i ≠ 1) :
    ∃ i ∈ s, 1 < f i := by
  contrapose! h₁
  obtain ⟨i, m, i_ne⟩ : ∃ i ∈ s, f i ≠ 1 := h₂
  apply ne_of_lt
  calc
    ∏ j ∈ s, f j < ∏ j ∈ s, 1 := prod_lt_prod' h₁ ⟨i, m, (h₁ i m).lt_of_ne i_ne⟩
    _ = 1 := prod_const_one

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