Cosine Theta in Projections List

StatusFully Proven
TypeTheorem
ModuleChebyshevCircles.Proofs.PolynomialConstruction

Statement

Theorem Cosine Theta in Projections List
[blueprint]

For $N > 0$, $\cos\theta \in \mathrm{realProjectionsList}(N, \theta).$

theorem realProjectionsList_mem_cos_theta (N : ℕ) (θ : ℝ) (hN : 0 < N) :
    Real.cos θ ∈ realProjectionsList N θ := by
Proof ▼ 


  unfold realProjectionsList
  simp only [List.mem_map, List.mem_range]
  use 0
  exact ⟨hN, by simp⟩

Dependencies (uses)

Dependents (used by)

Neighborhood

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