case intro
E : Type u_2
ι : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : Finite ι
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : MeasureTheory.Measure E
val✝ : Fintype ι
⊢ IsAddFundamentalDomain { x // x ∈ toAddSubgroup (span ℤ (Set.range ↑b)) } (fundamentalDomain b)
E : Type u_2
ι : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : Finite ι
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : MeasureTheory.Measure E
⊢ IsAddFundamentalDomain { x // x ∈ toAddSubgroup (span ℤ (Set.range ↑b)) } (fundamentalDomain b)
cases nonempty_fintype ι
no goals
case intro
E : Type u_2
ι : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : Finite ι
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : MeasureTheory.Measure E
val✝ : Fintype ι
⊢ IsAddFundamentalDomain { x // x ∈ toAddSubgroup (span ℤ (Set.range ↑b)) } (fundamentalDomain b)
exact IsAddFundamentalDomain.mk' (nullMeasurableSet (fundamentalDomain_measurableSet b))
  fun x => exist_unique_vadd_mem_fundamentalDomain b x