instBoundedRandomULiftOfULiftableOfMonad

Mathlib.Control.Random

URI: https://scilib.ai/kg/mathlib#Random.instBoundedRandomULiftOfULiftableOfMonad

Lean4

instance {α : Type u} [Preorder α] [ULiftable m m'] [BoundedRandom m α] [Monad m'] : BoundedRandom m' (ULift.{v} α)
    where
  randomR lo hi
    h := do
    let ⟨x⟩ ← ULiftable.up.{v} (BoundedRandom.randomR lo.down hi.down h)
    pure ⟨ULift.up x.val, x.prop⟩

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

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

Разделы

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

Аффилиация

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