rank_singleton

Mathlib.SetTheory.ZFC.Rank

URI: https://scilib.ai/kg/mathlib#PSet.rank_singleton

English

The rank of the singleton {x} is the successor of rank x.

Русский

Ранг множества {x} равен следующему рангу x.

LaTeX

$$$$ \operatorname{rank}(\{ x \}) = \operatorname{succ}(\operatorname{rank}(x)) $$$$

Lean4

@[simp]
theorem rank_singleton (x : PSet) : rank { x } = succ (rank x) :=
  (rank_insert _ _).trans (by simp)

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

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

Разделы

Аффилиация

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