lean_workbook_plus_62425
ProvedProve that is always less than or equal to 15.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_62425 : ∀ x : ℝ, (-8 * x ^ 2 + 15) ≤ 15 := by sorry
Source
Prove that is always less than or equal to 15.
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_62425 : ∀ x : ℝ, (-8 * x ^ 2 + 15) ≤ 15 := by sorry