mFourierSubalgebra_closure_eq_top

English

The Fourier subalgebra is dense in the algebra of continuous functions on UnitAddTorus: its topological closure is the whole space C(UnitAddTorus d, ℂ).

Русский

Фурье-подалгебра плотная в пространстве непрерывных функций на UnitAddTorus: его топологическое закрытие равно всему пространству C(UnitAddTorus d, ℂ).

LaTeX

$$$ (mFourierSubalgebra(d)).topologicalClosure = ⊤ $$$

Lean4

/-- The subalgebra of `C(UnitAddTorus d, ℂ)` generated by `mFourier n` for `n : d → ℤ` is dense. -/
theorem mFourierSubalgebra_closure_eq_top : (mFourierSubalgebra d).topologicalClosure = ⊤ :=
  ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints _ mFourierSubalgebra_separatesPoints

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