psum_left

Mathlib.Data.Finite.Sum

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

English

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

Русский

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

LaTeX

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

Lean4

theorem psum_left {α β : Sort*} [Finite (α ⊕' β)] : Finite α :=
  of_injective (PSum.inl : α → α ⊕' β) PSum.inl_injective

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

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

Разделы

Аффилиация

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