lift_id

Mathlib.SetTheory.Cardinal.Defs

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

English

A cardinal lifted within the same universe remains unchanged.

Русский

Кардинал, поднятый в той же самой вселенной, не меняется.

LaTeX

$$$\\mathrm{lift}_{u,u}(a) = a$ for all $a \\in \\mathrm{Cardinal}$$$

Lean4

/-- A cardinal lifted to the same universe equals itself. -/
@[simp]
theorem lift_id (a : Cardinal) : lift.{u, u} a = a :=
  lift_id'.{u, u} a

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

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

Разделы

Аффилиация

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