lift_eq_aleph0

Mathlib.SetTheory.Cardinal.Order

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

English

The lift of a equals aleph-null if and only if a equals aleph-null.

Русский

Лифт a равен ℵ₀ тогда и только тогда, когда a равен ℵ₀.

LaTeX

$$$\operatorname{lift}(a) = \aleph_0 \iff a = \aleph_0$$$

Lean4

@[simp]
theorem lift_eq_aleph0 {c : Cardinal.{u}} : lift.{v} c = ℵ₀ ↔ c = ℵ₀ := by simpa using lift_inj (b := ℵ₀)

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

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

Разделы

Аффилиация

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