English
The fundamental domain is a measurable set under the standard Borel measurable structure on E when ι is finite.
Русский
Фундаментальная область измерима в постановке Бореля на E, когда ι конечен.
LaTeX
$$$\operatorname{MeasurableSet}(\operatorname{fundamentalDomain}(b)).$$$
Lean4
@[measurability]
theorem fundamentalDomain_measurableSet [MeasurableSpace E] [OpensMeasurableSpace E] [Finite ι] :
MeasurableSet (fundamentalDomain b) := by
cases nonempty_fintype ι
haveI : FiniteDimensional ℝ E := FiniteDimensional.of_fintype_basis b
let D : Set (ι → ℝ) := Set.pi Set.univ fun _ : ι => Set.Ico (0 : ℝ) 1
rw [(_ : fundamentalDomain b = b.equivFun.toLinearMap ⁻¹' D)]
· refine measurableSet_preimage (LinearMap.continuous_of_finiteDimensional _).measurable ?_
exact MeasurableSet.pi Set.countable_univ fun _ _ => measurableSet_Ico
· ext
simp only [D, fundamentalDomain, Set.mem_Ico, Set.mem_setOf_eq, LinearEquiv.coe_coe, Set.mem_preimage,
Basis.equivFun_apply, Set.mem_pi, Set.mem_univ, forall_true_left]
