nonempty_equiv_of_countable — Mathlib

English

There exists a nonempty equivalence between any two countably infinite types α and β.

Русский

Существует непустая эквивалентность между двумя счетно-бесконечными типами α и β.

LaTeX

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

Lean4

instance nonempty_equiv_of_countable [Countable α] [Infinite α] [Countable β] [Infinite β] : Nonempty (α ≃ β) :=
  by
  cases nonempty_denumerable α
  cases nonempty_denumerable β
  exact ⟨(Denumerable.eqv _).trans (Denumerable.eqv _).symm⟩

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