English
If g is injective, tprod over Set.range g equals tprod over domain via g: ∏' x : Set.range g, f x = ∏' x, f (g x).
Русский
Если g инъективна, т-произведение по Set.range g равно т-произведению через g: ∏' x : Set.range g, f x = ∏' x, f (g x).
LaTeX
$$$\\\\prod' x : Set.range g, f x = \\\\prod' x, f (g x)$$$
Lean4
/-- If `f b = 1` for all `b ∈ t`, then the product of `f a` with `a ∈ s` is the same as the
product of `f a` with `a ∈ s ∖ t`. -/
@[to_additive /-- If `f b = 0` for all `b ∈ t`, then the sum of `f a` with `a ∈ s` is the same as
the sum of `f a` with `a ∈ s ∖ t`. -/
]
theorem tprod_setElem_eq_tprod_setElem_diff {f : β → α} (s t : Set β) (hf₀ : ∀ b ∈ t, f b = 1) :
∏' a : s, f a = ∏' a : (s \ t : Set β), f a :=
.symm <|
(Set.inclusion_injective (t := s) Set.diff_subset).tprod_eq (f := f ∘ (↑)) <|
mulSupport_subset_iff'.2 fun b hb ↦ hf₀ b <| by simpa using hb
