countable_iff_exists_injective — Mathlib

English

There is a canonical coercion from Set α to Type u given by s ↦ Elem(s).

Русский

Существует каноническое вложение из Set α в Type u, заданное отображением s ↦ Elem(s).

LaTeX

$$$\text{There exists a canonical coercion } \mathrm{Set}(\alpha) \to \mathrm{Type},\ s \mapsto \mathrm{Elem}(s).$$$

Lean4

protected theorem countable_iff_exists_injective {s : Set α} : s.Countable ↔ ∃ f : s → ℕ, Injective f :=
  countable_iff_exists_injective s

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