English
If f: α → β is injective and DecidablePred for Set.range f, then the finprod over β of a piecewise predicate along f equals the finprod over α, i.e., the domain embedding preserves finprod.
Русский
Если f: α → β инъективно и существует разрешимое предикат для образа Set.range f, то финпроизведение по β сопоставимо с по α.
LaTeX
$$$ (finprod f b) = (finprod a, g a) $$$
Lean4
@[to_additive]
theorem finprod_emb_domain' {f : α → β} (hf : Injective f) [DecidablePred (· ∈ Set.range f)] (g : α → M) :
(∏ᶠ b : β, if h : b ∈ Set.range f then g (Classical.choose h) else 1) = ∏ᶠ a : α, g a :=
by
simp_rw [← finprod_eq_dif]
rw [finprod_dmem, finprod_mem_range hf, finprod_congr fun a => _]
intro a
rw [dif_pos (Set.mem_range_self a), hf (Classical.choose_spec (Set.mem_range_self a))]
