English
Same as 2334 but with a different formatting variant: ∏ a ∈ s, f a = ∏ a : Subtype p, f a, given p and Fintype of Subtype p.
Русский
То же самое, что и в 2334, однако в другой форме: ∏ a ∈ s, f a = ∏ a : Subtype p, f a при условии существования типа-подтипа.
LaTeX
$$$\displaystyle \prod a ∈ s, f a = \prod a : Subtype p, f a$$$
Lean4
/-- The product of a function `g` defined only on a set `s` is equal to
the product of a function `f` defined everywhere,
as long as `f` and `g` agree on `s`, and `f = 1` off `s`. -/
@[to_additive /-- The sum of a function `g` defined only on a set `s` is equal to
the sum of a function `f` defined everywhere,
as long as `f` and `g` agree on `s`, and `f = 0` off `s`. -/
]
theorem prod_congr_set [Fintype ι] (s : Set ι) [DecidablePred (· ∈ s)] (f : ι → M) (g : s → M)
(w : ∀ x (hx : x ∈ s), f x = g ⟨x, hx⟩) (w' : ∀ x ∉ s, f x = 1) : ∏ i, f i = ∏ i, g i :=
by
rw [← prod_subset s.toFinset.subset_univ (by simpa), prod_subtype (p := (· ∈ s)) _ (by simp)]
congr! with ⟨x, h⟩
exact w x h
