continuum

Mathlib.SetTheory.Cardinal.Continuum

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

English

If a ≥ ℵ0 and 1 < b, then a < (b^a).ord.cof.

Русский

Если a ≥ ℵ0 и b > 1, то a < cof(ord(b^a)).

LaTeX

$$$$ \aleph_0 \le a \Rightarrow a < (b^a).ord.cof. $$$$

Lean4

/-- Cardinality of the continuum. -/
def continuum : Cardinal.{u} :=
  2 ^ ℵ₀

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

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

Разделы

Аффилиация

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