Mathlib Map

Theorems · Definition · probability

Random.casesOn

{m : Type u → Type u_1} →
  {α : Type u} →
    {motive : Random m α → Sort u_2} →
      (t : Random m α) → ((random : {g : Type} → [RandomGen g] → RandGT g m α) → motive { random := random }) → motive t
Defined in
Mathlib.Control.Random
Cited by
0 results in Mathlib
Foundations
Depth 5 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Random.noConfusion · cited by 0Random.noConfusionRandom.noConfusionType · cited by 0Random.noConfusionTypeRandGT · cited by 0RandGTRandom · cited by 0RandomRandom.casesOnCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • RandGTstatement and proof · cited by 0
  • Randomstatement and proof · cited by 0

Cited by2

Results whose statement or proof uses this declaration.