lean_workbook_plus_20550
ProvedProve that for all real numbers .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_20550 (a b c : ℝ) : 2 * |a + b + c| ≤ |a + b| + |b + c| + |c + a| := by sorry
Source
Prove that for all real numbers .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_20550 (a b c : ℝ) : 2 * |a + b + c| ≤ |a + b| + |b + c| + |c + a| := by sorry