hasCardinalLT_aleph0_iff

Mathlib.SetTheory.Cardinal.HasCardinalLT

URI: https://scilib.ai/kg/mathlib#hasCardinalLT_aleph0_iff

← MathLib Explorer

English

HasCardinalLT X aleph0 iff X is finite.

Русский

HasCardinalLT X aleph0 эквивалентно тому, что X конечен.

LaTeX

$$HasCardinalLT X \\aleph0 ↔ Finite X$$

Lean4

@[simp]
theorem hasCardinalLT_aleph0_iff (X : Type u) : HasCardinalLT X Cardinal.aleph0.{v} ↔ Finite X := by
  simpa [HasCardinalLT] using Cardinal.mk_lt_aleph0_iff

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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