fourierSubalgebra_separatesPoints

English

The Fourier subalgebra separates points of AddCircle(T); for any distinct x ≠ y in AddCircle(T), there exists a Fourier monomial that takes different values at x and y.

Русский

Подалгебра Фурье разделяет точки AddCircle(T); для любых различных x ≠ y существует мономиала Фурье, принимающая разные значения в x и в y.

LaTeX

$$({\n x ≠ y } → ∃ n ∈ ℤ, f_n(x) ≠ f_n(y))$$

Lean4

/-- The subalgebra of `C(AddCircle T, ℂ)` generated by `fourier n` for `n ∈ ℤ`
separates points. -/
theorem fourierSubalgebra_separatesPoints : (@fourierSubalgebra T).SeparatesPoints :=
  by
  intro x y hxy
  refine ⟨_, ⟨fourier 1, subset_adjoin ⟨1, rfl⟩, rfl⟩, ?_⟩
  dsimp only; rw [fourier_one, fourier_one]
  contrapose! hxy
  rw [Subtype.coe_inj] at hxy
  exact injective_toCircle hT.elim.ne' hxy

Похожие утверждения