Chebyshev Roots in [-1, 1]

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.ChebyshevRoots

Statement

Theorem Chebyshev Roots in [-1, 1]
[blueprint]

For all $N, k \in \mathbb{N}$, $\xi_k = \cos((2k+1)\pi/(2N)) \in [-1, 1]$. This is immediate from the range of the cosine function.

theorem chebyshevRoot_in_Icc (N k : ℕ) : chebyshevRoot N k ∈ Set.Icc (-1) 1 := by
Proof ▼ 


  unfold chebyshevRoot
  exact Real.cos_mem_Icc _

Dependencies (uses)

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