setOf_finite — Mathlib

English

The collection of finite subsets of a countable type is countable.

Русский

Множество конечных подмножеств счётного типа счётно.

LaTeX

$$$[\\text{Countable }\\alpha] \\Rightarrow \\{s:\\ Set\\alpha \\mid s\\Finite\\}.Countable$$$

Lean4

/-- The set of finite sets in a countable type is countable. -/
theorem setOf_finite [Countable α] : {s : Set α | s.Finite}.Countable := by
  simpa using countable_setOf_finite_subset countable_univ

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