instPSum

Mathlib.Data.Finite.Sum

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

instance {α β : Sort*} [Finite α] [Finite β] : Finite (α ⊕' β) :=
  of_equiv _ ((Equiv.psumEquivSum _ _).symm.trans (Equiv.plift.psumCongr Equiv.plift))

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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