lean_workbook_plus_3174
ProvedWhich can be prove with AM-GM
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_3174 (a b c: ℝ) : a^2 + b^2 ≥ 2*a*b ∧ b^2 + c^2 ≥ 2*b*c ∧ a^2 + c^2 ≥ 2*a*c := by sorry
Source
Which can be prove with AM-GM
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_3174 (a b c: ℝ) : a^2 + b^2 ≥ 2*a*b ∧ b^2 + c^2 ≥ 2*b*c ∧ a^2 + c^2 ≥ 2*a*c := by sorry