infinite_compl

Mathlib.Data.Set.Finite.Basic

URI: https://scilib.ai/kg/mathlib#Set.Finite.infinite_compl

English

If α is infinite and s is finite, then the complement s^c is infinite.

Русский

Если α бесконечен и s конечно, то дополнение s^c бесконечно.

LaTeX

$$$ [\text{Infinite}(\alpha)] \land s^c \text{ Finite} \Rightarrow s^c \text{ Infinite}$$$

Lean4

theorem infinite_compl [Infinite α] {s : Set α} (hs : s.Finite) : sᶜ.Infinite := fun h =>
  Set.infinite_univ (α := α) (by simpa using hs.union h)

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

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

Разделы

Аффилиация

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