English
If there is an equivalence e between index types and for all i the cardinalities satisfy #(f i) = #(g (e i)), then #(Π i, f i) = #(Π i, g i).
Русский
Если между индексами существует эквивалентность e и для всех i выполняется #(f i) = #(g(e i)), то #(Π i, f i) = #(Π i, g i).
LaTeX
$$$ \forall {\iota \iota' : Type u} {f : \iota → Type v} {g : \iota' → Type v} (e : \iota ≃ \iota'),(\forall i, \#(f i) = \#(g (e i))) : \#(\Pi i, f i) = \#(\Pi i, g i)$$$
Lean4
theorem mk_pi_congr {ι ι' : Type u} {f : ι → Type v} {g : ι' → Type v} (e : ι ≃ ι') (h : ∀ i, #(f i) = #(g (e i))) :
#(Π i, f i) = #(Π i, g i) :=
mk_congr <| Equiv.piCongr e fun i ↦ Classical.choice <| Cardinal.eq.mp (h i)
