lift_mk_shrink'

Mathlib.SetTheory.Cardinal.Basic

URI: https://scilib.ai/kg/mathlib#Cardinal.lift_mk_shrink'

English

A simplified variant: lift(#Shrink(α)) = lift(α) for small α.

Русский

Упрощённый вариант: lift(#Shrink(α)) = lift(α) при малом α.

LaTeX

$$$\\operatorname{lift}(\\#\\mathrm{Shrink}(\\alpha)) = \\operatorname{lift}(\\#\\alpha)$$$

Lean4

@[simp]
theorem lift_mk_shrink' (α : Type u) [Small.{v} α] : Cardinal.lift.{u} #(Shrink.{v} α) = Cardinal.lift.{v} #α :=
  lift_mk_shrink.{u, v, 0} α

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

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

Разделы

Аффилиация

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