English
The interior of the fundamental domain consists of those points of the domain that are not contained in any nontrivial translate. In symbols, fundamentalInterior(G,s) = s \\ ⋃_{g ≠ 1} g · s.
Русский
Внутренняя часть фундаментальной области состоит из тех точек области, которые не лежат в любом ненулевом переносе. Формально: fundamentalInterior(G,s) = s \\ ⋃_{g ≠ 1} g · s.
LaTeX
$$$\\mathrm{fundamentalInterior}(G,s) = s \\setminus \\bigcup_{\\substack{g \\in G \\\\ g \\neq 1}} g \\cdot s$$$
Lean4
/-- The interior of a fundamental domain, those points of the domain not lying in any translate. -/
@[to_additive MeasureTheory.addFundamentalInterior /-- The interior of a fundamental domain, those
points of the domain not lying in any translate. -/
]
def fundamentalInterior : Set α :=
s \ ⋃ (g : G) (_ : g ≠ 1), g • s
