small_plift

Mathlib.Logic.Small.Defs

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

English

If α is Small, then PLift α is Small.

Русский

Если α мала, то PLift α мала.

LaTeX

$$$Small(\alpha) \Rightarrow Small(PLift(\alpha)).$$$

Lean4

instance small_plift (α : Type u) [Small.{v} α] : Small.{v} (PLift α) :=
  small_map Equiv.plift

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

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

Разделы

Аффилиация

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