lift_lt_continuum

Mathlib.SetTheory.Cardinal.Continuum

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

English

If aleph0 ≤ c then c < c^(cof(ord c)).

Русский

Если aleph0 ≤ c, то c < c^(cof(ord c)).

LaTeX

$$$$ \aleph_0 \le c \Rightarrow c < c^{\operatorname{cof}(\operatorname{ord}(c))}. $$$$

Lean4

@[simp]
theorem lift_lt_continuum {c : Cardinal.{u}} : lift.{v} c < 𝔠 ↔ c < 𝔠 := by rw [← lift_continuum.{v, u}, lift_lt]

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

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

Разделы

Аффилиация

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