English
Let i be an injection from mulSupport g to β and assume mulSupport f ⊆ Set.range i with g(x) = f(i x); then ∏' x, f x = ∏' y, g y.
Русский
Пусть i — инъекция между опорами; если опора f вложена в образ i и g = f ∘ i, то т-произведения совпадают.
LaTeX
$$$\\\\prod' x, f x = \\\\prod' y, g y$$$
Lean4
@[to_additive]
theorem tprod_eq {g : γ → β} (hg : Injective g) {f : β → α} (hf : mulSupport f ⊆ Set.range g) :
∏' c, f (g c) = ∏' b, f b := by
classical
have : mulSupport f = g '' mulSupport (f ∘ g) := by rw [mulSupport_comp_eq_preimage, Set.image_preimage_eq_iff.2 hf]
rw [← Function.comp_def]
by_cases hf_fin : (mulSupport f).Finite
· have hfg_fin : (mulSupport (f ∘ g)).Finite := hf_fin.preimage hg.injOn
lift g to γ ↪ β using hg
simp_rw [tprod_eq_prod' hf_fin.coe_toFinset.ge, tprod_eq_prod' hfg_fin.coe_toFinset.ge, comp_apply, ←
Finset.prod_map]
refine Finset.prod_congr (Finset.coe_injective ?_) fun _ _ ↦ rfl
simp [this]
· have hf_fin' : ¬Set.Finite (mulSupport (f ∘ g)) := by rwa [this, Set.finite_image_iff hg.injOn] at hf_fin
simp_rw [tprod_def, SummationFilter.support_eq_univ, Set.inter_univ,
show (unconditional β).HasSupport by infer_instance, show (unconditional γ).HasSupport by infer_instance,
true_and, if_neg hf_fin, if_neg hf_fin', Multipliable]
simp [hg.hasProd_iff (mulSupport_subset_iff'.1 hf)]
