continuum_le_lift

Mathlib.SetTheory.Cardinal.Continuum

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

English

cof cont? 𝔠 ≤ lift c ↔ 𝔠 ≤ c: lifting preserves comparison with continuum.

Русский

Cof cont? 𝔠 ≤ lift c ⇔ 𝔠 ≤ c: подъем сохраняет сравнение с континуумом.

LaTeX

$$$$ \mathfrak{c} \le lift(c) \leftrightarrow \mathfrak{c} \le c. $$$$

Lean4

@[simp]
theorem continuum_le_lift {c : Cardinal.{u}} : 𝔠 ≤ lift.{v} c ↔ 𝔠 ≤ c := by rw [← lift_continuum.{v, u}, lift_le]

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

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

Разделы

Аффилиация

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