exists_eq_range — Mathlib

English

If s is countable and nonempty, then there exists f: ℕ → α such that s = range f.

Русский

Если s счетно и непусто, то существует f: ℕ → α такое, что s = range f.

LaTeX

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

Lean4

/-- If `s : Set α` is a nonempty countable set, then there exists a map
`f : ℕ → α` such that `s = range f`. -/
theorem exists_eq_range {s : Set α} (hc : s.Countable) (hs : s.Nonempty) : ∃ f : ℕ → α, s = range f :=
  by
  rcases hc.exists_surjective hs with ⟨f, hf⟩
  refine ⟨(↑) ∘ f, ?_⟩
  rw [hf.range_comp, Subtype.range_coe]

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