aleph0_le_lift

Mathlib.SetTheory.Cardinal.Order

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

English

For every cardinal c, ℵ₀ ≤ lift(c) if and only if ℵ₀ ≤ c.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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