infinite_iff

Mathlib.SetTheory.Cardinal.Basic

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

English

An index set α is infinite if and only if ℵ₀ ≤ |α|.

Русский

Множество α бесконечно тогда и только тогда, когда ℵ₀ ≤ |α|.

LaTeX

$$$ \mathrm{Infinite}(\alpha) \iff \aleph_0 \le |\alpha| $$$

Lean4

theorem infinite_iff {α : Type u} : Infinite α ↔ ℵ₀ ≤ #α := by
  rw [← not_lt, lt_aleph0_iff_finite, not_finite_iff_infinite]

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

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

Разделы

Аффилиация

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