lean_workbook_plus_3625
ProvedTo have the solution only,
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_3625 (r : ℝ) : (1 - 2 * r ≥ 0 ∧ r ≤ 1 / 2) ↔ r ≤ 1 / 2 := by sorry
Source
To have the solution only,
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_3625 (r : ℝ) : (1 - 2 * r ≥ 0 ∧ r ≤ 1 / 2) ↔ r ≤ 1 / 2 := by sorry