small_ulift

Mathlib.Logic.Small.Defs

URI: https://scilib.ai/kg/mathlib#small_ulift

English

If α is Small, then ULift_w α is Small (in the same universe).

Русский

Если α мала, то ULift_w α также мала (в той же вселенной).

LaTeX

$$$Small(\alpha) \Rightarrow Small(ULift^{w}(\alpha)).$$$

Lean4

instance small_ulift (α : Type u) [Small.{v} α] : Small.{v} (ULift.{w} α) :=
  small_map Equiv.ulift

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

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

Разделы

Аффилиация

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