lean_workbook_plus_53137
ProvedFor each , prove that there is some prime with .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_53137 (x : ℝ) (hx : 1 < x) : ∃ p, x < p ∧ p < 2 * x := by sorry
Source
For each , prove that there is some prime with .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_53137 (x : ℝ) (hx : 1 < x) : ∃ p, x < p ∧ p < 2 * x := by sorry