instNoMaxOrder

Mathlib.SetTheory.Cardinal.Order

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

English

There is no greatest cardinal: for every a there exists b with a < b.

Русский

У кардиналов нет наибольшего элемента: для каждого a существует b с a < b.

LaTeX

$$$\forall a \in \mathrm{Cardinal}, \exists b \in \mathrm{Cardinal}, a < b$$$

Lean4

instance : NoMaxOrder Cardinal.{u} where
  exists_gt
    a :=
    ⟨_, cantor a⟩
      -- short-circuit type class inference

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

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

Разделы

Аффилиация

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