English
If for every x in the space there exists a unique group element g with g • x ∈ s and s is measurable, then s is a fundamental domain for the G-action with respect to μ.
Русский
Если для каждого x существует единственный элемент группы g такой, что g • x ∈ s, и s измерима, то s является фундаментальной доменной областью для действия G на пространстве с мерой μ.
LaTeX
$$$\\text{IsFundamentalDomain}(G,s,μ)$$$
Lean4
/-- If for each `x : α`, exactly one of `g • x`, `g : G`, belongs to a measurable set `s`, then `s`
is a fundamental domain for the action of `G` on `α`. -/
@[to_additive /-- If for each `x : α`, exactly one of `g +ᵥ x`, `g : G`, belongs to a measurable set
`s`, then `s` is a fundamental domain for the additive action of `G` on `α`. -/
]
theorem mk' (h_meas : NullMeasurableSet s μ) (h_exists : ∀ x : α, ∃! g : G, g • x ∈ s) : IsFundamentalDomain G s μ
where
nullMeasurableSet := h_meas
ae_covers := Eventually.of_forall fun x => (h_exists x).exists
aedisjoint a b
hab :=
Disjoint.aedisjoint <|
disjoint_left.2 fun x hxa hxb => by
rw [mem_smul_set_iff_inv_smul_mem] at hxa hxb
exact hab (inv_injective <| (h_exists x).unique hxa hxb)
