lean_workbook_plus_61442
ProvedNote that if , then
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_61442 (a b : ℝ) (hab : a > 0 ∧ b > 0) : |a - b| < max (|a|) (|b|) := by sorry
Source
Note that if , then
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_61442 (a b : ℝ) (hab : a > 0 ∧ b > 0) : |a - b| < max (|a|) (|b|) := by sorry