denumerable — Mathlib

English

Any infinite subset of ℕ is denumerable; equivalently, there exists a bijection with ℕ.

Русский

Любое бесконечное подмножество ℕ денумерируемо; эквивалентно существованию биекции с ℕ.

LaTeX

$$$\exists e:\, s\cong\mathbb{N}$$$

Lean4

/-- Any infinite set of naturals is denumerable. -/
def denumerable (s : Set ℕ) [DecidablePred (· ∈ s)] [Infinite s] : Denumerable s :=
  Denumerable.ofEquiv ℕ
    { toFun := toFunAux
      invFun := ofNat s
      left_inv := leftInverse_of_surjective_of_rightInverse ofNat_surjective right_inverse_aux
      right_inv := right_inverse_aux }

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