measure_eq — Mathlib

English

If s and t are two fundamental domains for the same action, their measures are equal: μ(s) = μ(t).

Русский

Если s и t являются двумя фундаментальными областями одной и той же группы, их меры равны.

LaTeX

$$$$\\mu(s) = \\mu(t).$$$$

Lean4

/-- If `s` and `t` are two fundamental domains of the same action, then their measures are equal. -/
@[to_additive /-- If `s` and `t` are two fundamental domains of the same action, then their measures
      are equal. -/
    ]
protected theorem measure_eq (hs : IsFundamentalDomain G s μ) (ht : IsFundamentalDomain G t μ) : μ s = μ t := by
  simpa only [setLIntegral_one] using hs.setLIntegral_eq ht (fun _ => 1) fun _ _ => rfl

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