covolume_eq_volume — Mathlib

English

The interior of a fundamental domain is itself a fundamental domain for the same action with the same measure μ.

Русский

Внутренняя часть фундаментальной области сама образует фундаментальную область для того же действия и той же меры μ.

LaTeX

$$IsFundamentalDomain G (fundamentalInterior G s) μ$$

Lean4

/-- The `covolume` can be computed by taking the `volume` of any given fundamental domain `s`. -/
@[to_additive]
theorem covolume_eq_volume (ν : Measure α) [Countable G] [MeasurableSpace G] [MeasurableSMul G α]
    [SMulInvariantMeasure G α ν] {s : Set α} (fund_dom_s : IsFundamentalDomain G s ν) : covolume G α ν = ν s :=
  by
  dsimp [covolume]
  simp only [(fund_dom_s.hasFundamentalDomain ν), ↓reduceDIte]
  rw [fund_dom_s.measure_eq]
  exact (fund_dom_s.hasFundamentalDomain ν).ExistsIsFundamentalDomain.choose_spec

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