lift_aleph

Mathlib.SetTheory.Cardinal.Aleph

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

English

Lift of aleph at o equals aleph at lift(o): lift(aleph(o)) = aleph(lift(o)).

Русский

Подъем aleph от o равен aleph от подъема o: lift(aleph(o)) = aleph(lift(o)).

LaTeX

$$$$ \operatorname{lift}(\aleph(o)) = \aleph(\operatorname{lift}(o)). $$$$

Lean4

@[simp]
theorem lift_aleph (o : Ordinal.{u}) : lift.{v} (aleph o) = aleph (Ordinal.lift.{v} o) := by simp [aleph_eq_preAleph]

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

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

Разделы

Аффилиация

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