aleph0_eq_lift

Mathlib.SetTheory.Cardinal.Order

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

English

ℵ₀ = lift c if and only if ℵ₀ = c, for any cardinal c.

Русский

ℵ₀ = lift c тогда и только тогда, когда ℵ₀ = c, для любого кардинала c.

LaTeX

$$$\forall c,\ \aleph_0 = \operatorname{lift} c \iff \aleph_0 = c$$$

Lean4

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

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

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

Разделы

Аффилиация

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