iUnion_smul_ae_eq — Mathlib

English

If (G acts) and s is a fundamental domain, then the union over all g ∈ G of g • s covers almost everywhere the space: ⋃ g g • s =ᵐ μ univ.

Русский

Если s является фундаментальной доменной областью, то объединение по всем g ∈ G изобразено почти повсеместно на всём пространстве: ⋃ g g • s =ᵐ μ univ.

LaTeX

$$$\\bigcup_{g \\in G} (g \\cdot s) =^{\\mu}_{a.e.} \\text{univ}$$$

Lean4

@[to_additive]
theorem iUnion_smul_ae_eq (h : IsFundamentalDomain G s μ) : ⋃ g : G, g • s =ᵐ[μ] univ :=
  eventuallyEq_univ.2 <| h.ae_covers.mono fun _ ⟨g, hg⟩ => mem_iUnion.2 ⟨g⁻¹, _, hg, inv_smul_smul _ _⟩

Похожие утверждения