uncountable_iff_isEmpty_embedding

English

A type α is uncountable if and only if the type of embeddings α ↪ ℕ is empty.

Русский

Тип α неисчислим; это эквивалентно тому, что множество вложений α ↪ ℕ пусто.

LaTeX

$$$$ \mathrm{Uncountable}(\alpha) \iff \mathrm{IsEmpty}(\alpha \hookrightarrow \mathbb{N}) $$$$

Lean4

theorem uncountable_iff_isEmpty_embedding : Uncountable α ↔ IsEmpty (α ↪ ℕ) := by
  rw [← not_countable_iff, countable_iff_nonempty_embedding, not_nonempty_iff]

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