`BookProof.ChapterShannonSampling.exists_rep` (z : AddCircle T) : ∃ ξ : ℝ, ξ ∈ Ioc (-(T / 2)) (-(T / 2) + T) ∧ (ξ : AddCircle T) = z

Initializing...

`BookProof.ChapterShannonSampling.exists_rep` (z : AddCircle T) : ∃ ξ : ℝ, ξ ∈ Ioc (-(T / 2)) (-(T / 2) + T) ∧ (ξ : AddCircle T) = z · Prove2Me