English
Reorder a product via a bijection i : s → κ with appropriate surjectivity and injectivity hypotheses: ∏_{x∈s} f x = ∏_{x∈κ} g x.
Русский
Переупорядочить произведение через биекцию i : s → κ при надлежащих гипотезах сюръекции и инъекции: ∏_{x∈s} f x = ∏_{x∈κ} g x.
LaTeX
$$$\\exists i:\\, \\mathrm{Finset}\\,s \\to \\mathrm{Finset}\\,\\kappa\\; \\text{биективно},\\; \\text{и } (\\forall x∈s, f x = g (i x))\\Rightarrow \\prod_{x∈s} f x = \\prod_{x∈κ} g x$$$
Lean4
/-- Reorder a product.
The difference with `Finset.prod_bij'` is that the bijection is specified as a surjective injection,
rather than by an inverse function.
The difference with `Finset.prod_nbij` is that the bijection is allowed to use membership of the
domain of the product, rather than being a non-dependent function. -/
@[to_additive /-- Reorder a sum.
The difference with `Finset.sum_bij'` is that the bijection is specified as a surjective injection,
rather than by an inverse function.
The difference with `Finset.sum_nbij` is that the bijection is allowed to use membership of the
domain of the sum, rather than being a non-dependent function. -/
]
theorem prod_bij (i : ∀ a ∈ s, κ) (hi : ∀ a ha, i a ha ∈ t) (i_inj : ∀ a₁ ha₁ a₂ ha₂, i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂)
(i_surj : ∀ b ∈ t, ∃ a ha, i a ha = b) (h : ∀ a ha, f a = g (i a ha)) : ∏ x ∈ s, f x = ∏ x ∈ t, g x :=
congr_arg Multiset.prod (Multiset.map_eq_map_of_bij_of_nodup f g s.2 t.2 i hi i_inj i_surj h)
