English
If a finite set s has cardinality at most 1 and the product over s equals b, then every element of s has value b.
Русский
Если мощность конечного множества s не превосходит 1 и произведение по s равно b, то каждый элемент множества имеет значение b.
LaTeX
$$$\\#s \\le 1 \\rightarrow \\left(\\prod_{x \\in s} f(x) = b\\right) \\rightarrow \\forall x \\in s,\\ f(x) = b$$$
Lean4
/-- If a product of a `Finset` of size at most 1 has a given value, so
do the terms in that product. -/
@[to_additive eq_of_card_le_one_of_sum_eq /-- If a sum of a `Finset` of size at most 1 has a given
value, so do the terms in that sum. -/
]
theorem eq_of_card_le_one_of_prod_eq {s : Finset ι} (hc : #s ≤ 1) {f : ι → M} {b : M} (h : ∏ x ∈ s, f x = b) :
∀ x ∈ s, f x = b := by
intro x hx
by_cases hc0 : #s = 0
· exact False.elim (card_ne_zero_of_mem hx hc0)
· have h1 : #s = 1 := le_antisymm hc (Nat.one_le_of_lt (Nat.pos_of_ne_zero hc0))
rw [card_eq_one] at h1
grind
