hasProd_one_iff — Mathlib

English

Let f: ι → α with f(i) ≥ 1 for all i. Then the infinite product ∏' i, f(i) equals 1 if and only if f(i) = 1 for every i.

Русский

Пусть f: ι → α удовлетворяет f(i) ≥ 1 для всех i. Тогда бесконечное произведение ∏' i, f(i) равно 1 тогда и только тогда, когда f(i) = 1 для каждого i.

LaTeX

$$$\\\\prod' i \\, f(i) = 1 \\\\iff \\\\forall i \\, f(i) = 1$$$

Lean4

@[to_additive]
theorem hasProd_one_iff : HasProd f 1 ↔ ∀ x, f x = 1 :=
  (hasProd_one_iff_of_one_le fun _ ↦ one_le _).trans funext_iff

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