English
Variant of prod_nbij' that uses two index maps i and j with left and right inverses, resulting in equality of products when f a = g (i a).
Русский
Вариант prod_nbij' с двумя отображениями i и j и условиями левого и правого обратного соответствия, приводящий к равенству произведений.
LaTeX
$$$\\forall i, j, hi, hj, left\\_inv, right\\_inv, h:\\forall a∈s, f a = g (i a) \\Rightarrow \\prod_{x∈s} f x = \\prod_{x∈t} g x$$$
Lean4
/-- Reorder a product.
The difference with `Finset.prod_nbij` is that the bijection is specified with an inverse, rather
than as a surjective injection.
The difference with `Finset.prod_bij'` is that the bijection and its inverse are non-dependent
functions, rather than being allowed to use membership of the domains of the products.
The difference with `Finset.prod_equiv` is that bijectivity is only required to hold on the domains
of the products, rather than on the entire types.
-/
@[to_additive /-- Reorder a sum.
The difference with `Finset.sum_nbij` is that the bijection is specified with an inverse, rather
than as a surjective injection.
The difference with `Finset.sum_bij'` is that the bijection and its inverse are non-dependent
functions, rather than being allowed to use membership of the domains of the sums.
The difference with `Finset.sum_equiv` is that bijectivity is only required to hold on the domains
of the sums, rather than on the entire types. -/
]
theorem prod_nbij' (i : ι → κ) (j : κ → ι) (hi : ∀ a ∈ s, i a ∈ t) (hj : ∀ a ∈ t, j a ∈ s)
(left_inv : ∀ a ∈ s, j (i a) = a) (right_inv : ∀ a ∈ t, i (j a) = a) (h : ∀ a ∈ s, f a = g (i a)) :
∏ x ∈ s, f x = ∏ x ∈ t, g x :=
prod_bij' (fun a _ ↦ i a) (fun b _ ↦ j b) hi hj left_inv right_inv h
