infinite_of_finite_compl — Mathlib

English

If α is infinite and the complement of s in α is finite, then s is infinite.

Русский

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

LaTeX

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

Lean4

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

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