lean_workbook_plus_26915
ProvedSimilar, and
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_26915 (b c : ℝ) : (8 / 9 * b ^ 2 + 9 / 2) ≥ 4 * b ∧ (8 / 9 * c ^ 2 + 9 / 2) ≥ 4 * c := by sorry
Source
Similar, and
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_26915 (b c : ℝ) : (8 / 9 * b ^ 2 + 9 / 2) ≥ 4 * b ∧ (8 / 9 * c ^ 2 + 9 / 2) ≥ 4 * c := by sorry