lift_lt_aleph1

Mathlib.SetTheory.Cardinal.Aleph

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

English

For any c, lift(c) < ℵ₁ iff c < ℵ₁.

Русский

Для любого кардинала c верно: lift(c) < ℵ₁ тогда и только тогда, когда c < ℵ₁.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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