randBound

Mathlib.Control.Random

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

Lean4

/-- Generate a random value of type `α` between `x` and `y` inclusive. -/
def randBound (α : Type u) [Preorder α] [BoundedRandom m α] (lo hi : α) (h : lo ≤ hi) [RandomGen g] :
    RandGT g m { a // lo ≤ a ∧ a ≤ hi } :=
  (BoundedRandom.randomR lo hi h : RandGT g _ _)

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

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

Разделы

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

Аффилиация

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