Real Projections Lie in [-1,1]

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.RootsOfUnity

Statement

Theorem Real Projections Lie in [-1,1]
[blueprint]

$\cos(\theta + 2\pi k/N) \in [-1, 1]$ for all $N$, $\theta$, $k$.

theorem realProjection_mem_Icc (N : ℕ) (θ : ℝ) (k : ℕ) :
    Real.cos (θ + 2 * π * k / N) ∈ Set.Icc (-1 : ℝ) 1 := by
Proof ▼ 


  exact ⟨Real.neg_one_le_cos _, Real.cos_le_one _⟩

Dependencies (uses)

None

Dependents (used by)

None

Neighborhood

Legend
Not Ready
Work in Progress
Sorry (theorems only)
Proven/Defined
Fully Proven (theorems only)
Axiom
Mathlib Ready
Theorems/Lemmas
Definitions
Axioms