instPSigma

Mathlib.Data.Finite.Sigma

URI: https://scilib.ai/kg/mathlib#Finite.instPSigma

English

If α and β are finite, then the PSum α β is finite.

Русский

Если α и β конечны, то PSum α β конечен.

LaTeX

$$$ [Finite α] \Rightarrow [Finite β] \Rightarrow Finite (PSum α β) $$$

Lean4

instance {ι : Sort*} {π : ι → Sort*} [Finite ι] [∀ i, Finite (π i)] : Finite (Σ' i, π i) :=
  of_equiv _ (Equiv.psigmaEquivSigmaPLift π).symm

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

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

Разделы

Аффилиация

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