English
Let I be finite and f: κ → ι, g: ι → M. If the pairwise condition holds for I, then the product over the filtered set where f j = f n equals g(f n).
Русский
Пусть I конечен, f: κ → ι, g: ι → M. При условии попарной совместимости произведение по отфильтрованному множеству j: f j = f n равняется g(f n).
LaTeX
$$$\\prod_{j \\in I, \\; f(j)=f(n)} g(f(j)) = g(f(n))$$$
Lean4
/-- A version of `Finset.prod_map` and `Finset.prod_image`, but we do not assume that `f` is
injective. Rather, we assume that the images of `f` are disjoint on `I`, and `g ⊥ = 1`. The
conclusion is the same as in `prod_image`. -/
@[to_additive (attr := simp) /-- A version of `Finset.sum_map` and `Finset.sum_image`, but we do not assume that `f` is
injective. Rather, we assume that the images of `f` are disjoint on `I`, and `g ⊥ = 0`. The
conclusion is the same as in `sum_image`. -/
]
theorem prod_image_of_disjoint [DecidableEq ι] [PartialOrder ι] [OrderBot ι] {f : κ → ι} {g : ι → M} (hg_bot : g ⊥ = 1)
{I : Finset κ} (hf_disj : (I : Set κ).PairwiseDisjoint f) : ∏ s ∈ I.image f, g s = ∏ i ∈ I, g (f i) :=
by
refine prod_image_of_pairwise_eq_one <| hf_disj.imp fun i j hdisj hfij ↦ ?_
rw [Function.onFun, ← hfij, disjoint_self] at hdisj
rw [hdisj, hg_bot]
