English
Let s be a finite set of elements of ι and p a predicate on ι with DecidablePred. If every element of s satisfies p, then the product taken over the subtype s subset {x ∈ ι | p x} of the function f is equal to the product taken over s itself, i.e. ∏_{x ∈ s.subtype p} f x = ∏_{x ∈ s} f x.
Русский
Пусть s — конечное множество элементов из ι, и p — предикат на ι с разрешимым доказательством. Если каждый элемент s удовлетворяет p, то произведение по подтипу s, состоящему из элементов с p, равно произведению по самому множеству s: ∏_{x ∈ s.subtype p} f x = ∏_{x ∈ s} f x.
LaTeX
$$$\displaystyle \text{If } h: \forall x\in s,\ p(x)\text{ then } \prod_{x\in s,\ p(x)} f(x) = \prod_{x\in s} f(x).$$$
Lean4
/-- If all elements of a `Finset` satisfy the predicate `p`, a product
over `s.subtype p` equals that product over `s`. -/
@[to_additive /-- If all elements of a `Finset` satisfy the predicate `p`, a sum
over `s.subtype p` equals that sum over `s`. -/
]
theorem prod_subtype_of_mem (f : ι → M) {p : ι → Prop} [DecidablePred p] (h : ∀ x ∈ s, p x) :
∏ x ∈ s.subtype p, f x = ∏ x ∈ s, f x :=
by
rw [prod_subtype_eq_prod_filter, filter_true_of_mem]
simpa using h
