aleph1_eq_lift

Mathlib.SetTheory.Cardinal.Aleph

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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