lean_workbook_plus_75525
Provedwhich is true as
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_75525 (k : ℝ) : 2 ≤ abs (1 + k) + 2 * abs (1 - k) := by sorry
Source
which is true as
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_75525 (k : ℝ) : 2 ≤ abs (1 + k) + 2 * abs (1 - k) := by sorry