def definition def or abbrev

`p_switch`

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

formal statement (Lean)

 140def p_switch : ℚ := switchWinningSet.card / (Finset.univ : Finset Outcome).card

Definition body.

 141
 142/-- **STAY-WINS-WITH-PROBABILITY-1/3.** -/

From the project-wide theorem graph. These declarations reference this one in their body.

montyHallCert in IndisputableMonolith.Decision.MontyHall decl_use
MontyHallCert in IndisputableMonolith.Decision.MontyHall decl_use
monty_hall_one_statement in IndisputableMonolith.Decision.MontyHall decl_use
p_switch_eq in IndisputableMonolith.Decision.MontyHall decl_use
p_switch_real in IndisputableMonolith.Decision.MontyHall decl_use
switch_eq_two_stay in IndisputableMonolith.Decision.MontyHall decl_use
switch_strictly_better in IndisputableMonolith.Decision.MontyHall decl_use
switch_strictly_better_real in IndisputableMonolith.Decision.MontyHall decl_use
total_probability in IndisputableMonolith.Decision.MontyHall decl_use

Lean names referenced from this declaration's body.