countable_iff_exists_injOn — Mathlib

English

A set s is countable iff there exists an injective map f: s → ℕ.

Русский

Множество s счётно тогда и только тогда, когда существует инъективная карта f: s → ℕ.

LaTeX

$$$s.Countable \iff \exists f : s \to \mathbb{N}, \operatorname{Injective}(f)$$$

Lean4

/-- A set `s : Set α` is countable if and only if there exists a function `α → ℕ` injective
on `s`. -/
theorem countable_iff_exists_injOn {s : Set α} : s.Countable ↔ ∃ f : α → ℕ, InjOn f s :=
  Set.countable_iff_exists_injective.trans exists_injOn_iff_injective.symm

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