English
The Fourier subalgebra separates points of UnitAddTorus: for any distinct x,y, there exists f in mFourierSubalgebra with f(x) ≠ f(y).
Русский
Подалгебра Фурье разделяет точки в UnitAddTorus: для любых различных x,y существует функция из mFourierSubalgebra, отличающая x и y.
LaTeX
$$$ \text{SeparatesPoints}(\text{mFourierSubalgebra}(d)) $$$
Lean4
/-- The subalgebra of `C(UnitAddTorus d, ℂ)` generated by `mFourier n` for `n ∈ ℤᵈ` separates
points. -/
theorem mFourierSubalgebra_separatesPoints : (mFourierSubalgebra d).SeparatesPoints := by
classical
intro x y hxy
rw [Ne, funext_iff, not_forall] at hxy
obtain ⟨i, hi⟩ := hxy
refine ⟨_, ⟨mFourier (Pi.single i 1), subset_adjoin ⟨Pi.single i 1, rfl⟩, rfl⟩, ?_⟩
dsimp only
rw [mFourier_single, mFourier_single, fourier_one, fourier_one, Ne, Subtype.coe_inj]
contrapose! hi
exact AddCircle.injective_toCircle one_ne_zero hi
