lt_cof_type

Mathlib.SetTheory.Cardinal.Cofinality

URI: https://scilib.ai/kg/mathlib#Ordinal.lt_cof_type

English

If a subset S of α is not unbounded, then #S is not greater than cof(type r).

Русский

Если S не является неограниченным, то |S| не превосходит cof(type r).

LaTeX

$$$#S < cof(type\\; r) \\Rightarrow Bounded\\ r\\ S$$$

Lean4

theorem lt_cof_type [IsWellOrder α r] {S : Set α} : #S < cof (type r) → Bounded r S := by
  simpa using not_imp_not.2 cof_type_le

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

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

Разделы

Аффилиация

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