countable_setOf_finite_subset — Mathlib

English

The family of finite subsets of a countable set is countable.

Русский

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

LaTeX

$$$\\forall s:\\ Set\\alpha,\\ s.\\Countable \\to \\{ t:\\ Set\\alpha\\mid t\\text{ finite }\\land t\\subseteq s\\}.Countable$$$

Lean4

/-- The set of finite subsets of a countable set is countable. -/
theorem countable_setOf_finite_subset {s : Set α} (hs : s.Countable) : {t | Set.Finite t ∧ t ⊆ s}.Countable :=
  by
  have := hs.to_subtype
  refine (countable_range fun t : Finset s => Subtype.val '' (t : Set s)).mono ?_
  rintro t ⟨ht, hts⟩
  lift t to Set s using hts
  lift t to Finset s using ht.of_finite_image Subtype.val_injective.injOn
  exact mem_range_self _

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