English
Let s be a finite subset of ι and f: ι → M. If for every i, f(i) ≠ 1 implies i ∈ s (equivalently, f(i) = 1 for i ∉ s), then the product over i ∈ s equals the product over all i: ∏ i ∈ s, f i = ∏ i, f i.
Русский
Пусть s — конечное подмножество ι и f: ι → M. Если для каждого i выполняется f(i) ≠ 1 ⇒ i ∈ s (эквивалентно: для i ∉ s выполняется f(i) = 1), то произведение по i ∈ s равно произведению по всем i: ∏ i ∈ s, f i = ∏ i, f i.
LaTeX
$$$$ \\left(\\forall i, f(i) \\neq 1 \\Rightarrow i \\in s\\right) \\Rightarrow \\prod_{i \\in s} f(i) = \\prod_i f(i). $$$$
Lean4
@[to_additive]
theorem prod_subset {s : Finset ι} {f : ι → M} (h : ∀ i, f i ≠ 1 → i ∈ s) : ∏ i ∈ s, f i = ∏ i, f i :=
Finset.prod_subset s.subset_univ <| by simpa [not_imp_comm (a := _ ∈ s)]
