measure_fundamentalInterior — Mathlib

English

The covolume of the action equals the volume of any fundamental domain: covolume(G,α,ν) = ν(s) for any IsFundamentalDomain G s ν.

Русский

Ковольюм действия равен объему любой фундаментальной области: covolume(G,α,ν) = ν(s).

LaTeX

$$\\covolume G α ν = ν s$$

Lean4

@[to_additive MeasureTheory.IsAddFundamentalDomain.measure_addFundamentalInterior]
theorem measure_fundamentalInterior : μ (fundamentalInterior G s) = μ s :=
  measure_diff_null' hs.measure_fundamentalFrontier

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