card_le_aleph0

Mathlib.Computability.Encoding

URI: https://scilib.ai/kg/mathlib#Computability.FinEncoding.card_le_aleph0

English

For every finite encoding e of α, the cardinality of α is at most ℵ0.

Русский

Для каждого конечного кодирования e α, кардинал α не превосходит ℵ0.

LaTeX

$$$\forall e:\mathrm{FinEncoding}(\alpha), \#\alpha \le \aleph_0$$$

Lean4

theorem card_le_aleph0 {α : Type u} (e : FinEncoding α) : #α ≤ ℵ₀ :=
  e.toEncoding.card_le_aleph0

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru