preAleph_succ

Mathlib.SetTheory.Cardinal.Aleph

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

English

preAleph(succ o) = succ(preAleph o).

Русский

preAleph(succ o) = succ(preAleph o).

LaTeX

$$$ \text{preAleph}(\operatorname{succ}(o)) = \operatorname{succ}(\text{preAleph}(o)) $$$

Lean4

@[simp]
theorem preAleph_succ (o : Ordinal) : preAleph (succ o) = succ (preAleph o) :=
  preAleph.map_succ o

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

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

Разделы

Аффилиация

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