lift_eq_aleph1

Mathlib.SetTheory.Cardinal.Aleph

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

English

lift(c) equals ℵ₁ iff c equals ℵ₁.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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