English
Similar to mk_pi_congr but with indexing types in different universes: if e : ι ≃ ι' and for all i, #(f i) = #(g (e i)), then #(Π i, f i) = #(Π i, g i).
Русский
Аналогично mk_pi_congr, но индексы в разных вселенных: если e : ι ≃ ι' и для всех i #(f i) = #(g(e i)), то #(Π i, f i) = #(Π i, g i).
LaTeX
$$$ \forall {\iota : Type u} {\iota' : Type v} {f : \iota → Type w} {g : \iota' → Type w} (e : \iota ≃ \iota') (h : \forall i, \#(f i) = \#(g (e i))) : \#(\Pi i, f i) = \#(\Pi i, g i)$$$
Lean4
/-- Similar to `mk_pi_congr` with indexing types in different universes. This is not a strict
generalization. -/
theorem mk_pi_congr' {ι : Type u} {ι' : Type v} {f : ι → Type max w (max u v)} {g : ι' → Type max w (max u 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)
