cof_eq

Mathlib.SetTheory.Cardinal.Regular

URI: https://scilib.ai/kg/mathlib#Cardinal.IsRegular.cof_eq

English

For a regular cardinal c, cof c equals c; equivalently cof_ord_le c is an equality with the regularity condition forcing equality.

Русский

Для регулярного кардинала cof c равен c; иначе cof_ord ≤ c превращается в равенство благодаря регулярности.

LaTeX

$$$\text{cof} c = c.$$$

Lean4

theorem cof_eq {c : Cardinal} (H : c.IsRegular) : c.ord.cof = c :=
  (cof_ord_le c).antisymm H.2

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

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

Разделы

Аффилиация

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