mk_pi_congrRight — Mathlib

English

If for all i we have #(f i) = #(g i), then #(Π i, f i) = #(Π i, g i).

Русский

Если для каждого i выполняется #(f i) = #(g i), то #(Π i, f i) = #(Π i, g i).

LaTeX

$$$ \forall {\iota : Type u} {f g : \iota → Type v} (h : \forall i, \#(f i) = \#(g i)) : \, \#(\Pi i, f i) = \#(\Pi i, g i)$$$

Lean4

theorem mk_pi_congrRight {ι : Type u} {f g : ι → Type v} (h : ∀ i, #(f i) = #(g i)) : #(Π i, f i) = #(Π i, g i) :=
  mk_pi_congr (Equiv.refl ι) h

Похожие утверждения