English
If ι and ι' are propositions and e is an equivalence between them, and for all i we have #(f i) = #(g (e i)), then #(Π i, f i) = #(Π i, g i).
Русский
Если ι и ι' – пропозиции и существует эквивелентность между ними, и для всех i выполняется #(f i) = #(g(e i)), то #(Π i, f i) = #(Π i, g i).
LaTeX
$$$ \forall {\iota \iota' : Prop} (f : \iota → Type v) (g : \iota' → Type v) (e : \iota \leftrightarrow \iota') (h : \forall i, \#(f i) = \#(g (e.mp i))) : \#(\Pi i, f i) = \#(\Pi i, g i)$$$
Lean4
theorem mk_pi_congr_prop {ι ι' : Prop} {f : ι → Type v} {g : ι' → Type v} (e : ι ↔ ι')
(h : ∀ i, #(f i) = #(g (e.mp i))) : #(Π i, f i) = #(Π i, g i) :=
mk_congr <| Equiv.piCongr (.ofIff e) fun i ↦ Classical.choice <| Cardinal.eq.mp (h i)
