denumerable_iff — Mathlib

English

There exists a denumerable structure on α if and only if |α| = ℵ₀.

Русский

Существует денумерабельная структура на α тогда и только тогда |α| = ℵ₀.

LaTeX

$$$ \exists \text{Denumerable}(\alpha) \iff |\alpha| = \aleph_0$$$

Lean4

theorem denumerable_iff {α : Type u} : Nonempty (Denumerable α) ↔ #α = ℵ₀ :=
  ⟨fun ⟨h⟩ => mk_congr ((@Denumerable.eqv α h).trans Equiv.ulift.symm), fun h =>
    by
    obtain ⟨f⟩ := Quotient.exact h
    exact ⟨Denumerable.mk' <| f.trans Equiv.ulift⟩⟩

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