nonempty_denumerable — Mathlib

English

There exists a denumerable structure on α if and only if α is countable and infinite.

Русский

Существует денумерируемая структура на α тогда и только тогда, когда α счетно и бесконечно.

LaTeX

$$$\text{Nonempty}(\text{Denumerable}(\alpha)) \ \iff\ (\text{Countable}(\alpha) \wedge \text{Infinite}(\alpha))$$$

Lean4

/-- See also `nonempty_encodable`, `nonempty_fintype`. -/
theorem nonempty_denumerable (α : Type*) [Countable α] [Infinite α] : Nonempty (Denumerable α) :=
  (nonempty_encodable α).map fun h => @Denumerable.ofEncodableOfInfinite _ h _

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