lift_aleph0

Mathlib.SetTheory.Cardinal.Defs

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

English

Lifting aleph-null yields aleph-null: lift(aleph0) = aleph0.

Русский

Подъём алеф-ноль даёт алеф-ноль: lift(aleph0) = aleph0.

LaTeX

$$$ \operatorname{lift}(\aleph_{0}) = \aleph_{0} $$$

Lean4

@[simp]
theorem lift_aleph0 : lift ℵ₀ = ℵ₀ :=
  lift_lift _

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

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

Разделы

Аффилиация

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