univ

Mathlib.SetTheory.Ordinal.Basic

URI: https://scilib.ai/kg/mathlib#Cardinal.IsStrongLimit.univ

English

The universal cardinal is a strong limit: for every c < univ, 2^c < univ.

Русский

Универсальная кардинальность является сильным пределом: для каждого c < univ, 2^c < univ.

LaTeX

$$IsStrongLimit(\\mathrm{univ})$$

Lean4

theorem univ : IsStrongLimit univ.{u, v} :=
  ⟨univ_ne_zero, fun c h ↦
    let ⟨w, h⟩ := lt_univ'.1 h;
    lt_univ'.2 ⟨2 ^ w, by simp [h]⟩⟩

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

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

Разделы

Аффилиация

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