continuum_pos

Mathlib.SetTheory.Cardinal.Continuum

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

English

There exists a positive continuum; i.e., 0 < 𝔠.

Русский

Существование положительного континуума; т.е. 0 < 𝔠.

LaTeX

$$$$ 0 < \mathfrak{c}. $$$$

Lean4

theorem continuum_pos : 0 < 𝔠 :=
  nat_lt_continuum 0

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

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

Разделы

Аффилиация

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