English
Let p be a predicate on ι and s be a finite set of elements of the subtype {x // p x}. For f and g as functions with g agreeing with f on the embedded subtype, the product of g over the mapped subtype equals the product of f over s: ∏ x ∈ s.map (Embedding.subtype _) , g x = ∏ x ∈ s , f x.
Русский
Пусть p — предикат на ι, и s — конечное множество подтипов {x | p x}. Для функций f : {x // p x} → M и g : ι → M, если g совпадает с f на образе подтипа, то произведение g по отображению над подтипом равняется произведению f по s: ∏ x ∈ s.map (Embedding.subtype _), g x = ∏ x ∈ s, f x.
LaTeX
$$$\displaystyle \forall h:\, \forall x:\,{x\in s},\ g x = f x \implies \Big(\prod x\in s.map(Embedding.subtype _),\, g\,x\Big) = \prod x\in s,\, f x.$$$
Lean4
/-- A product of a function over a `Finset` in a subtype equals a
product in the main type of a function that agrees with the first
function on that `Finset`. -/
@[to_additive /-- A sum of a function over a `Finset` in a subtype equals a
sum in the main type of a function that agrees with the first
function on that `Finset`. -/
]
theorem prod_subtype_map_embedding {p : ι → Prop} {s : Finset { x // p x }} {f : { x // p x } → M} {g : ι → M}
(h : ∀ x : { x // p x }, x ∈ s → g x = f x) : (∏ x ∈ s.map (Function.Embedding.subtype _), g x) = ∏ x ∈ s, f x :=
by
rw [Finset.prod_map]
exact Finset.prod_congr rfl h
