lt_aleph0_iff_finite

Mathlib.SetTheory.Cardinal.Basic

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

English

A type α has cardinality less than aleph0 if and only if α is finite.

Русский

Тип α имеет кардинал меньше aleph0 тогда и только тогда, когда α конечен.

LaTeX

$$$ #\alpha < \aleph_0 \iff \text{Finite } \alpha $$$

Lean4

theorem lt_aleph0_iff_finite {α : Type u} : #α < ℵ₀ ↔ Finite α := by
  simp only [lt_aleph0, mk_eq_nat_iff, finite_iff_exists_equiv_fin]

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

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

Разделы

Аффилиация

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