English
Let G be a group acting on a space α and s ⊆ α. The boundary of the fundamental domain is the part of s that lies in a nontrivial translate of s; equivalently, the frontier is the intersection s ∩ ⋃_{g ∈ G, g ≠ 1} g · s.
Русский
Пусть G действует на пространство α и подмножество s ⊆ α. Граница фундаментальной области состоит из тех точек в s, которые лежат в ненулевом сдвиге s; эквивалентно frontier = s ∩ ⋃_{g ∈ G, g ≠ 1} g · s.
LaTeX
$$$\\mathrm{fundamentalFrontier}(G,s) = s \\cap \\bigcup_{\\substack{g \\in G \\\\ g \\neq 1}} g \\cdot s$$$
Lean4
/-- The boundary of a fundamental domain, those points of the domain that also lie in a nontrivial
translate. -/
@[to_additive MeasureTheory.addFundamentalFrontier /-- The boundary of a fundamental domain, those
points of the domain that also lie in a nontrivial translate. -/
]
def fundamentalFrontier : Set α :=
s ∩ ⋃ (g : G) (_ : g ≠ 1), g • s
