mk_cardinal

Mathlib.SetTheory.Cardinal.Aleph

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

English

The cardinality of the set of cardinals equals the universe: |Cardinal| = univ.

Русский

Множество кардиналов имеет размер равный вселенной: |Cardinal| = univ.

LaTeX

$$$ \#\text{Cardinal} = \text{univ} $$$

Lean4

@[simp]
theorem mk_cardinal : #Cardinal = univ.{u, u + 1} := by
  simpa only [card_type, card_univ] using congr_arg card type_cardinal

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

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

Разделы

Аффилиация

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