lean_workbook_plus_19348
DisprovedPreamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_19348 : ∀ p : ℝ, p > 0 ∧ p ≠ 1 → 1 / 27 * ((9 - p) / 2) ^ 2 ≤ 1 / p := by sorry
Source
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_19348 : ∀ p : ℝ, p > 0 ∧ p ≠ 1 → 1 / 27 * ((9 - p) / 2) ^ 2 ≤ 1 / p := by sorry