nonempty_denumerable_iff — Mathlib

English

If α and β are countable and infinite, then there exists an equivalence α ≃ β.

Русский

Если α и β счетны и бесконечны, то существует эквивалентность α ≃ β.

LaTeX

$$$\exists e:\, \alpha \simeq \beta$$$

Lean4

theorem nonempty_denumerable_iff {α : Type*} : Nonempty (Denumerable α) ↔ Countable α ∧ Infinite α :=
  ⟨fun ⟨_⟩ ↦ ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ ↦ nonempty_denumerable _⟩

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