lean_workbook_plus_60949
OpenProve that for all real number of , then .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_60949 (x : ℝ) : abs (sin x) + abs (cos x) ≥ 1 := by sorry
Source
Prove that for all real number of , then .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_60949 (x : ℝ) : abs (sin x) + abs (cos x) ≥ 1 := by sorry