module module

`IndisputableMonolith.Decision.MontyHall`

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 (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (25)

abbrev Outcome L79
theorem outcome_count L82
def StayWins L86
def stayWinningSet L92
def SwitchWins L98
def switchWinningSet L104
theorem stay_or_switch L110
theorem not_both L117
theorem stayWinningSet_card L125
theorem switchWinningSet_card L130
def p_stay L137
def p_switch L140
theorem p_stay_eq L143
theorem p_switch_eq L149
theorem switch_strictly_better L159
theorem total_probability L165
theorem switch_eq_two_stay L170
def p_stay_real L177
def p_switch_real L180
theorem p_stay_real_eq L182
theorem p_switch_real_eq L188
theorem switch_strictly_better_real L194
structure MontyHallCert L212
def montyHallCert L225
theorem monty_hall_one_statement L249