instInfiniteFinset — Mathlib

English

If α is an infinite type, then the collection of all finite subsets of α is infinite.

Русский

Пусть α бесконечного типа. Тогда множество всех конечных подмножеств α бесконечно.

LaTeX

$$$ \\forall \\alpha\\ (\\operatorname{Infinite}(\\alpha) \\Rightarrow \\operatorname{Infinite}(\\mathrm{Finset}\\,\\alpha)) $$$

Lean4

instance [Infinite α] : Infinite (Finset α) :=
  Infinite.of_injective singleton Finset.singleton_injective

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