finite_or_infinite

Mathlib.Data.Finite.Defs

URI: https://scilib.ai/kg/mathlib#finite_or_infinite

English

For any α, either α is finite or α is infinite.

Русский

Для любого α верно: либо α конечна, либо α бесконечна.

LaTeX

$$$\\operatorname{Finite}(\\alpha) \\lor \\operatorname{Infinite}(\\alpha).$$$

Lean4

theorem finite_or_infinite (α : Sort*) : Finite α ∨ Infinite α :=
  or_iff_not_imp_left.2 not_finite_iff_infinite.1

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

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

Разделы

Аффилиация

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