lean_workbook_plus_10625
ProvedProve that for real numbers, implies .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_10625 (a b : ℝ) (h : |a| ≤ b) : -b ≤ a ∧ a ≤ b := by sorry
Source
Prove that for real numbers, implies .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_10625 (a b : ℝ) (h : |a| ≤ b) : -b ≤ a ∧ a ≤ b := by sorry