prod_const'

Mathlib.SetTheory.Cardinal.Defs

URI: https://scilib.ai/kg/mathlib#Cardinal.prod_const'

English

The same as Prod Const but without universes lifting: (prod (λ _, a)) = a^{#ι}.

Русский

То же самое, что Prod Const, без подъёмов по вселенным: (prod (λ _, a)) = a^{|ι|}.

LaTeX

$$$ \prod_{i: \iota} a = a^{|\iota|} $$$

Lean4

theorem prod_const' (ι : Type u) (a : Cardinal.{u}) : (prod fun _ : ι => a) = a ^ #ι :=
  inductionOn a fun _ => (mk_pi _).symm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru