continuum_lt_lift

Mathlib.SetTheory.Cardinal.Continuum

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

English

Another form: lift c < 𝔠 iff c < 𝔠.

Русский

Другая форма: lift c < 𝔠 ⇔ c < 𝔠.

LaTeX

$$$$ lift(c) < \mathfrak{c} \iff c < \mathfrak{c}. $$$$

Lean4

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

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

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

Разделы

Аффилиация

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