countable_iff_nonempty_encodable — Mathlib

English

A set is countable iff there exists a nonempty Encodable structure on its elements.

Русский

Множество счётно тогда и только тогда, когда для его элементов существует ненулевой кодирующий объект Encodable.

LaTeX

$$$s.Countable \iff Nonempty (Encodable\ s)$$$

Lean4

theorem countable_iff_nonempty_encodable {s : Set α} : s.Countable ↔ Nonempty (Encodable s) :=
  Encodable.nonempty_encodable.symm

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