tprod_range — Mathlib

English

If g : γ → β is injective on s, the tprod over g''s image equals the tprod over s: ∏' x : g '' s, f x = ∏' x : s, f (g x).

Русский

Если g инъективна на s, т-произведение по образу g равно по s: ∏' x : g''s, f x = ∏' x : s, f (g x).

LaTeX

$$$\\\\prod' x : g '' s, f x = \\\\prod' x : s, f (g x)$$$

Lean4

@[to_additive]
theorem tprod_range {g : γ → β} (f : β → α) (hg : Injective g) : ∏' x : Set.range g, f x = ∏' x, f (g x) :=
  by
  rw [← Set.image_univ, tprod_image f hg.injOn]
  simp_rw [← comp_apply (g := g), tprod_univ (f ∘ g)]

Похожие утверждения