lean_workbook_plus_60316
ProvedLet be the probability that is odd when is randomly chosen from the interval . We can see that this is the same as the probability that is odd when is randomly chosen from the interval . Furthermore, , which shows that is odd if and only if is even. Hence, the probability that is odd when is randomly chosen from the interval is equal to . Therefore, the probability that is odd when is randomly chosen from the interval can also be expressed as: Solving for gives us . Therefore, the probability that is odd when is randomly chosen from is .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_60316 (p : ℝ) (h₀ : p = 1 / 4 * (1 - p)) : p = 1 / 5 := by sorry
Source