finprod_mem_eq_of_bijOn — Mathlib

English

If g is injective, then ∏_{i∈range g} f(i) = ∏_{j} f(g(j)).

Русский

Если g инъективна, то произведение по диапазону равно произведению по применению к g.

LaTeX

$$\operatorname{Injective}(g) \Rightarrow \prod_{i \in \operatorname{range} g} f(i) = \prod_{j} f(g(j))$$

Lean4

/-- See also `Finset.prod_bij`. -/
@[to_additive /-- See also `Finset.sum_bij`. -/
    ]
theorem finprod_mem_eq_of_bijOn {s : Set α} {t : Set β} {f : α → M} {g : β → M} (e : α → β) (he₀ : s.BijOn e t)
    (he₁ : ∀ x ∈ s, f x = g (e x)) : ∏ᶠ i ∈ s, f i = ∏ᶠ j ∈ t, g j :=
  by
  rw [← Set.BijOn.image_eq he₀, finprod_mem_image he₀.2.1]
  exact finprod_mem_congr rfl he₁

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