countable_iff_exists_subset_range

English

Let α be a nonempty type and s ⊆ α. Then s is countable if and only if there exists a function f: ℕ → α with s ⊆ range f.

Русский

Пусть α — ненулевого типа, и s ⊆ α. Тогда s счетно тогда и только тогда, когда существует отображение f: ℕ → α такое, что s ⊆ диапазон f.

LaTeX

$$$\\operatorname{Nonempty}(\\alpha) \\wedge \\operatorname{Countable}(s) \\iff \\exists f:\\\\mathbb{N} \\\\to \\alpha,\\ s \\subseteq \\operatorname{range}(f)$$$

Lean4

theorem countable_iff_exists_subset_range [Nonempty α] {s : Set α} : s.Countable ↔ ∃ f : ℕ → α, s ⊆ range f :=
  ⟨fun h => by
    inhabit α
    exact ⟨enumerateCountable h default, subset_range_enumerate _ _⟩, fun ⟨f, hsf⟩ => (countable_range f).mono hsf⟩

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