ord_pos

Mathlib.SetTheory.Cardinal.Regular

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

English

If c is regular, then 0 < c.ord; in particular c.ord is nonzero.

Русский

Если c регулярный, то 0 < c.ord; ординал c.ord ненулевой.

LaTeX

$$$0 < c.ord$$$

Lean4

theorem ord_pos {c : Cardinal} (H : c.IsRegular) : 0 < c.ord :=
  by
  rw [Cardinal.lt_ord, card_zero]
  exact H.pos

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

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

Разделы

Аффилиация

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