lift_le_aleph0

Mathlib.SetTheory.Cardinal.Order

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

English

For any cardinal c, lift(c) ≤ ℵ0 if and only if c ≤ ℵ0.

Русский

Для любого кардинала c выполняется lift(c) ≤ ℵ₀ тогда и только тогда, когда c ≤ ℵ₀.

LaTeX

$$$\forall c,\ \operatorname{lift}(c) \le \aleph_0 \iff c \le \aleph_0$$$

Lean4

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

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

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

Разделы

Аффилиация

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