English
The pair (spanℤ(range b)), fundamentalDomain(b) forms an additive fundamental domain with respect to any Haar measure μ on E, when ι is finite.
Русский
Пара (spanℤ(range b), fundamentalDomain(b)) образует аддитивную фундаментальную область относительно любого преобразования Хаара μ на E при конечном ι.
LaTeX
$$$\text{IsAddFundamentalDomain}(\operatorname{span}_{\mathbb{Z}}(\operatorname{range} b), \operatorname{fundamentalDomain}(b), \mu).$$$
Lean4
/-- For a ℤ-lattice `Submodule.span ℤ (Set.range b)`, proves that the set defined
by `ZSpan.fundamentalDomain` is a fundamental domain. -/
protected theorem isAddFundamentalDomain [Finite ι] [MeasurableSpace E] [OpensMeasurableSpace E] (μ : Measure E) :
IsAddFundamentalDomain (span ℤ (Set.range b)) (fundamentalDomain b) μ :=
by
cases nonempty_fintype ι
exact
IsAddFundamentalDomain.mk' (nullMeasurableSet (fundamentalDomain_measurableSet b)) fun x =>
exist_unique_vadd_mem_fundamentalDomain b x
