ofEncodableOfInfinite — Mathlib

English

If α is countable and infinite, then there exists a denumerable structure on α.

Русский

Если α счетно и бесконечно, существует денумерируемая структура на α.

LaTeX

$$$\exists e:\, \text{Denumerable}(\alpha)$$$

Lean4

/-- An infinite encodable type is denumerable. -/
def ofEncodableOfInfinite (α : Type*) [Encodable α] [Infinite α] : Denumerable α :=
  by
  letI := @decidableRangeEncode α _
  letI : Infinite (Set.range (@encode α _)) := Infinite.of_injective _ (Equiv.ofInjective _ encode_injective).injective
  letI := Nat.Subtype.denumerable (Set.range (@encode α _))
  exact Denumerable.ofEquiv (Set.range (@encode α _)) (equivRangeEncode α)

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