psum_right

Mathlib.Data.Finite.Sum

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

English

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

Русский

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

LaTeX

$$$ [Finite (Σ' i, π i)] \Rightarrow Finite (π i) $$$

Lean4

theorem psum_right {α β : Sort*} [Finite (α ⊕' β)] : Finite β :=
  of_injective (PSum.inr : β → α ⊕' β) PSum.inr_injective

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

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

Разделы

Аффилиация

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