module module

`IndisputableMonolith.Mathematics.ProbabilityTheoryFromRS`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import

declarations in this module (6)

inductive KolmogorovAxiom L25
theorem kolmogorovAxiomCount L29
theorem certain_event_zero_cost L32
theorem uncertain_event_positive_cost L35
structure ProbabilityCert L38
def probabilityCert L43