measure_eq_tsum — Mathlib

English

For fundamental domain h and set t, μ t = ∑' g μ (g•t ∩ s).

Русский

Для фундаментальной области h и множества t выполняется μ(t) = ∑' g μ(g•t ∩ s).

LaTeX

$$$$\\mu(t) = \\sum_{g\\in G} \\mu\\bigl(g \\cdot t \\cap s\\bigr).$$$$

Lean4

@[to_additive]
theorem measure_eq_tsum (h : IsFundamentalDomain G s μ) (t : Set α) : μ t = ∑' g : G, μ (g • t ∩ s) := by
  simpa only [setLIntegral_one] using h.setLIntegral_eq_tsum' (fun _ => 1) t

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