card_le_aleph0 — Mathlib

English

For every encoding e of α, if e.Γ is countable, then #α ≤ ℵ0.

Русский

Для каждого кодирования e α, если e.Γ счётно, то #α ≤ ℵ0.

LaTeX

$$$\forall e:\mathrm{Encoding}(\alpha), \ [\mathrm{Countable}(e.\Gamma)] \rightarrow \#\alpha \le \aleph_0$$$

Lean4

theorem card_le_aleph0 {α : Type u} (e : Encoding.{u, v} α) [Countable e.Γ] : #α ≤ ℵ₀ :=
  haveI : Countable α := e.encode_injective.countable
  Cardinal.mk_le_aleph0

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