English
Let T > 0. The interval Ioc(0, T) serves as a fundamental domain for the subgroup Tℤ inside ℝ, providing a tiling of the real line by translates of this interval via the period T.
Русский
Пусть T > 0. Интервал Ioc(0, T) является фундаментальной областью подгруппы Tℤ в ℝ, образуя разбиение действительной оси на перенесения через период T.
LaTeX
$$$\\mathrm{Ioc}(0,T) \\text{ is a fundamental domain for } \\mathbb{Z} \\cdot T \\subseteq \\mathbb{R}$$$
Lean4
instance : HasAddFundamentalDomain (AddSubgroup.op <| .zmultiples T) ℝ where
ExistsIsAddFundamentalDomain := ⟨Ioc 0 (0 + T), isAddFundamentalDomain_Ioc' Fact.out 0⟩
