adaptUp

Mathlib.Control.ULiftable

URI: https://scilib.ai/kg/mathlib#ULiftable.adaptUp

Lean4

/-- convenient shortcut to avoid manipulating `ULift` -/
def adaptUp (F : Type v₀ → Type v₁) (G : Type max v₀ u₀ → Type u₁) [ULiftable F G] [Monad G] {α β} (x : F α)
    (f : α → G β) : G β :=
  up x >>= f ∘ ULift.down.{u₀}

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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