fourierSubalgebra_closure_eq_top — Mathlib

English

The topological closure of the Fourier subalgebra equals the whole algebra of continuous functions on AddCircle(T).

Русский

Плотность Фурье-подалгебры: её топологическая замыкa равна всей алгебре непрерывных функций на AddCircle(T).

LaTeX

$$fourierSubalgebra.topologicalClosure = ⊤$$

Lean4

/-- The subalgebra of `C(AddCircle T, ℂ)` generated by `fourier n` for `n ∈ ℤ` is dense. -/
theorem fourierSubalgebra_closure_eq_top : (@fourierSubalgebra T).topologicalClosure = ⊤ :=
  ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints fourierSubalgebra
    fourierSubalgebra_separatesPoints

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