not_isSuccLimit_of_lt_aleph0

Mathlib.SetTheory.Cardinal.Basic

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

← MathLib Explorer

English

Let c be a cardinal with c < aleph0. Then c is not a succ-limit cardinal.

Русский

Пусть c — кардинал с c < aleph0. Тогда c не является succ-limit кардиналом.

LaTeX

$$$ c < \aleph_0 \Rightarrow \neg \mathrm{IsSuccLimit}(c) $$$

Lean4

theorem not_isSuccLimit_of_lt_aleph0 {c : Cardinal} (h : c < ℵ₀) : ¬IsSuccLimit c :=
  by
  obtain ⟨n, rfl⟩ := lt_aleph0.1 h
  exact not_isSuccLimit_natCast n

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

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

Разделы

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

Аффилиация

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