G : Type u_1
H : Type ?u.244096
α : Type u_2
β : Type ?u.244102
E : Type ?u.244105
inst✝¹⁰ : Group G
inst✝⁹ : Group H
inst✝⁸ : MulAction G α
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MulAction H β
inst✝⁵ : MeasurableSpace β
inst✝⁴ : NormedAddCommGroup E
s t✝ : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
ν : Measure α
h : IsFundamentalDomain G s
t : Set α
ht : ∀ (g : G), g • t = t
hts : ↑↑μ (t ∩ s) = 0
⊢ (∑' (g : G), ↑↑μ (g • t ∩ s)) = 0
G : Type u_1
H : Type ?u.244096
α : Type u_2
β : Type ?u.244102
E : Type ?u.244105
inst✝¹⁰ : Group G
inst✝⁹ : Group H
inst✝⁸ : MulAction G α
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MulAction H β
inst✝⁵ : MeasurableSpace β
inst✝⁴ : NormedAddCommGroup E
s t✝ : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
ν : Measure α
h : IsFundamentalDomain G s
t : Set α
ht : ∀ (g : G), g • t = t
hts : ↑↑μ (t ∩ s) = 0
⊢ ↑↑μ t = 0
rw [measure_eq_tsum h]
no goals
G : Type u_1
H : Type ?u.244096
α : Type u_2
β : Type ?u.244102
E : Type ?u.244105
inst✝¹⁰ : Group G
inst✝⁹ : Group H
inst✝⁸ : MulAction G α
inst✝⁷ : MeasurableSpace α
inst✝⁶ : MulAction H β
inst✝⁵ : MeasurableSpace β
inst✝⁴ : NormedAddCommGroup E
s t✝ : Set α
μ : Measure α
inst✝³ : MeasurableSpace G
inst✝² : MeasurableSMul G α
inst✝¹ : SMulInvariantMeasure G α μ
inst✝ : Countable G
ν : Measure α
h : IsFundamentalDomain G s
t : Set α
ht : ∀ (g : G), g • t = t
hts : ↑↑μ (t ∩ s) = 0
⊢ (∑' (g : G), ↑↑μ (g • t ∩ s)) = 0
simp [ht, hts]