lift_lt_aleph0

Mathlib.SetTheory.Cardinal.Order

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

English

ℵ₀ equals lift(c) if and only if ℵ₀ equals c.

Русский

ℵ₀ равен lift(c) тогда и только тогда, когда ℵ₀ равен c.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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