card_lt_aleph0

Mathlib.SetTheory.Ordinal.Basic

URI: https://scilib.ai/kg/mathlib#Ordinal.card_lt_aleph0

English

For every c, c < univ iff ∃ c' with c = lift(c').

Русский

Для каждого c, c < univ тогда, когда существует c', что c = lift(c').

LaTeX

$$$c < \\mathrm{univ} \\iff \\exists c',\\ c = \\mathrm{lift}(c')$$$

Lean4

@[simp]
theorem card_lt_aleph0 {o} : card o < ℵ₀ ↔ o < ω :=
  le_iff_le_iff_lt_iff_lt.1 aleph0_le_card

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

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

Разделы

Аффилиация

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