infinite_or_finite

Mathlib.Data.Finite.Defs

URI: https://scilib.ai/kg/mathlib#Set.infinite_or_finite

English

Every set is either infinite or finite (the other dichotomy).

Русский

Каждое множество бесконечно или конечно.

LaTeX

$$$ \\text{Infinite}(s) \\lor \\text{Finite}(s) $$$

Lean4

protected theorem infinite_or_finite (s : Set α) : s.Infinite ∨ s.Finite :=
  em' _

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

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

Разделы

Аффилиация

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