prod_const — Mathlib

English

The product over i in ι of a equals lift(a) raised to the power of lift of the cardinality of ι: (prod fun _ : ι => a) = lift a ^ lift #ι.

Русский

Произведение по i в ι константы a равно подъёму константы a в степени подъёма кардинала множества ι: (prod _ a) = lift(a)^{lift(|ι|)}.

LaTeX

$$$ \prod_{i: \iota} a = \operatorname{lift}(a)^{\operatorname{lift}(|\iota|)} $$$

Lean4

@[simp]
theorem prod_const (ι : Type u) (a : Cardinal.{v}) : (prod fun _ : ι => a) = lift.{u} a ^ lift.{v} #ι :=
  inductionOn a fun _ => mk_congr <| Equiv.piCongr Equiv.ulift.symm fun _ => outMkEquiv.trans Equiv.ulift.symm

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