English
Specialization of a general rearrangement principle: if i : s → κ and hi ensures i a ∈ t, and h maps f a to g (i a), then ∏_{x∈s} f x = ∏_{x∈t} g x.
Русский
Специализация принципа перестановки: если i : s → κ и hi гарантирует i a ∈ t, а h устанавливает f a = g(i a), то произведения равны.
LaTeX
$$$\\forall i: s \\to \\kappa,\\; hi: ∀ a ∈ s, i a ∈ t,\\; \\forall h: ∀ a ∈ s, f a = g (i a)\\;\\Rightarrow \\; \\prod_{x\\in s} f x = \\prod_{x\\in t} g x$$$
Lean4
/-- Reorder a product.
The difference with `Finset.prod_nbij'` is that the bijection is specified as a surjective
injection, rather than by an inverse function.
The difference with `Finset.prod_bij` is that the bijection is a non-dependent function, rather than
being allowed to use membership of the domain of the product. -/
@[to_additive /-- Reorder a sum.
The difference with `Finset.sum_nbij'` is that the bijection is specified as a surjective injection,
rather than by an inverse function.
The difference with `Finset.sum_bij` is that the bijection is a non-dependent function, rather than
being allowed to use membership of the domain of the sum. -/
]
theorem prod_nbij (i : ι → κ) (hi : ∀ a ∈ s, i a ∈ t) (i_inj : (s : Set ι).InjOn i) (i_surj : (s : Set ι).SurjOn i t)
(h : ∀ a ∈ s, f a = g (i a)) : ∏ x ∈ s, f x = ∏ x ∈ t, g x :=
prod_bij (fun a _ ↦ i a) hi i_inj (by simpa using i_surj) h
