English
Specialization of the general bijection principle via a given equivalence e: ι ≃ κ; if s and t correspond under e and f agrees with g along e, then the products are equal: ∏_{i∈s} f i = ∏_{i∈t} g i.
Русский
Специализация принципа перестановки через данное эквивалентное отображение e: ι ≃ κ; если множества соответствуют под e и f согласуется с g, то произведения равны.
LaTeX
$$$\\text{prod\_equiv} (e)\\ (hst)\\ (hfg):\\; \\prod_{i \\in s} f i = \\prod_{i \\in t} g i$$$
Lean4
/-- Specialization of `Finset.prod_nbij'` that automatically fills in most arguments.
See `Fintype.prod_equiv` for the version where `s` and `t` are `univ`. -/
@[to_additive /-- `Specialization of `Finset.sum_nbij'` that automatically fills in most arguments.
See `Fintype.sum_equiv` for the version where `s` and `t` are `univ`. -/
]
theorem prod_equiv (e : ι ≃ κ) (hst : ∀ i, i ∈ s ↔ e i ∈ t) (hfg : ∀ i ∈ s, f i = g (e i)) :
∏ i ∈ s, f i = ∏ i ∈ t, g i := by refine prod_nbij' e e.symm ?_ ?_ ?_ ?_ hfg <;> simp [hst]
