ofENat_le_aleph0

Mathlib.SetTheory.Cardinal.ENat

URI: https://scilib.ai/kg/mathlib#Cardinal.ofENat_le_aleph0

English

For every n ∈ ENat, the corresponding cardinal is at most aleph-zero: ↑n ≤ ℵ₀.

Русский

Для любого n ∈ ℕ∞ соответствующий кардинал не превосходит ℵ₀: ↑n ≤ ℵ₀.

LaTeX

$$$\forall n : \mathbb{N}_\infty, \uparrow n \le \aleph_0$$$

Lean4

@[simp]
theorem ofENat_le_aleph0 (n : ℕ∞) : ↑n ≤ ℵ₀ :=
  ofENat_le_ofENat.2 le_top

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

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

Разделы

Аффилиация

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