English
Reorder a finite product by a bijection that is not necessarily invertible in a strong sense but satisfies a pair of compatibility conditions with two index sets: ∏_{x∈s} f x = ∏_{x∈t} g x under a suitable interrelation i, j.
Русский
Переупорядочить произведение конечной мощности по парам отображений i, j между множествами s и t при соответствующих условиях совместимости.
LaTeX
$$$\\prod x \\in s, f x = \\prod x \\in t, g x$ при наличии функций i, j и условий совместимости.$$
Lean4
/-- Reorder a product.
The difference with `Finset.prod_bij` is that the bijection is specified with an inverse, rather
than as a surjective injection.
The difference with `Finset.prod_nbij'` is that the bijection and its inverse are allowed to use
membership of the domains of the products, rather than being non-dependent functions. -/
@[to_additive /-- Reorder a sum.
The difference with `Finset.sum_bij` is that the bijection is specified with an inverse, rather than
as a surjective injection.
The difference with `Finset.sum_nbij'` is that the bijection and its inverse are allowed to use
membership of the domains of the sums, rather than being non-dependent functions. -/
]
theorem prod_bij' (i : ∀ a ∈ s, κ) (j : ∀ a ∈ t, ι) (hi : ∀ a ha, i a ha ∈ t) (hj : ∀ a ha, j a ha ∈ s)
(left_inv : ∀ a ha, j (i a ha) (hi a ha) = a) (right_inv : ∀ a ha, i (j a ha) (hj a ha) = a)
(h : ∀ a ha, f a = g (i a ha)) : ∏ x ∈ s, f x = ∏ x ∈ t, g x :=
by
refine prod_bij i hi (fun a1 h1 a2 h2 eq ↦ ?_) (fun b hb ↦ ⟨_, hj b hb, right_inv b hb⟩) h
rw [← left_inv a1 h1, ← left_inv a2 h2]
simp only [eq]
