English
Specialization of a bijection-based rearrangement: given e : ι → κ that is bijective, with index correspondence, the product is preserved.
Русский
Специализация перестановки через биекцияe: задано биективное отображение, сохраняющее соответствие индексов, произведение сохраняется.
LaTeX
$$$\\forall e: ι \\to κ\\, (he: e.Bijective)\\; (hst)\\ (hfg) \\Rightarrow \\prod_{i ∈ s} f i = \\prod_{i ∈ t} g i$$$
Lean4
/-- Specialization of `Finset.prod_bij` that automatically fills in most arguments.
See `Fintype.prod_bijective` for the version where `s` and `t` are `univ`. -/
@[to_additive /-- `Specialization of `Finset.sum_bij` that automatically fills in most arguments.
See `Fintype.sum_bijective` for the version where `s` and `t` are `univ`. -/
]
theorem prod_bijective (e : ι → κ) (he : e.Bijective) (hst : ∀ i, i ∈ s ↔ e i ∈ t) (hfg : ∀ i ∈ s, f i = g (e i)) :
∏ i ∈ s, f i = ∏ i ∈ t, g i :=
prod_equiv (.ofBijective e he) hst hfg
