lean_workbook_plus_15898
Openthis is a trigonometric ineq which equivalent to :
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_15898 (α : ℝ) : -1 ≤ Real.cos α ∧ Real.cos α ≤ 1 := by sorry
Source
this is a trigonometric ineq which equivalent to :
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_15898 (α : ℝ) : -1 ≤ Real.cos α ∧ Real.cos α ≤ 1 := by sorry