E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
this : FiniteDimensional ℝ E
⊢ MeasurableSet (fundamentalDomain b)
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
⊢ MeasurableSet (fundamentalDomain b)
haveI : FiniteDimensional ℝ E := FiniteDimensional.of_fintype_basis b
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
this : FiniteDimensional ℝ E
f : E →ₗ[ℝ] ι → ℝ := LinearMap.comp ↑(Finsupp.linearEquivFunOnFinite ℝ ℝ ι) ↑b.repr
⊢ MeasurableSet (fundamentalDomain b)
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
this : FiniteDimensional ℝ E
⊢ MeasurableSet (fundamentalDomain b)
let f := (Finsupp.linearEquivFunOnFinite ℝ ℝ ι).toLinearMap.comp b.repr.toLinearMap
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
this : FiniteDimensional ℝ E
f : E →ₗ[ℝ] ι → ℝ := LinearMap.comp ↑(Finsupp.linearEquivFunOnFinite ℝ ℝ ι) ↑b.repr
D : Set (ι → ℝ) := Set.pi Set.univ fun x => Set.Ico 0 1
⊢ MeasurableSet (fundamentalDomain b)
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
this : FiniteDimensional ℝ E
f : E →ₗ[ℝ] ι → ℝ := LinearMap.comp ↑(Finsupp.linearEquivFunOnFinite ℝ ℝ ι) ↑b.repr
⊢ MeasurableSet (fundamentalDomain b)
let D : Set (ι → ℝ) := Set.pi Set.univ fun _ : ι => Set.Ico (0 : ℝ) 1
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
this : FiniteDimensional ℝ E
f : E →ₗ[ℝ] ι → ℝ := LinearMap.comp ↑(Finsupp.linearEquivFunOnFinite ℝ ℝ ι) ↑b.repr
D : Set (ι → ℝ) := Set.pi Set.univ fun x => Set.Ico 0 1
⊢ MeasurableSet (↑f ⁻¹' D)

E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
this : FiniteDimensional ℝ E
f : E →ₗ[ℝ] ι → ℝ := LinearMap.comp ↑(Finsupp.linearEquivFunOnFinite ℝ ℝ ι) ↑b.repr
D : Set (ι → ℝ) := Set.pi Set.univ fun x => Set.Ico 0 1
⊢ fundamentalDomain b = ↑f ⁻¹' D
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
this : FiniteDimensional ℝ E
f : E →ₗ[ℝ] ι → ℝ := LinearMap.comp ↑(Finsupp.linearEquivFunOnFinite ℝ ℝ ι) ↑b.repr
D : Set (ι → ℝ) := Set.pi Set.univ fun x => Set.Ico 0 1
⊢ MeasurableSet (fundamentalDomain b)
rw [(_ : fundamentalDomain b = f ⁻¹' D)]
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
this : FiniteDimensional ℝ E
f : E →ₗ[ℝ] ι → ℝ := LinearMap.comp ↑(Finsupp.linearEquivFunOnFinite ℝ ℝ ι) ↑b.repr
D : Set (ι → ℝ) := Set.pi Set.univ fun x => Set.Ico 0 1
⊢ MeasurableSet D
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
this : FiniteDimensional ℝ E
f : E →ₗ[ℝ] ι → ℝ := LinearMap.comp ↑(Finsupp.linearEquivFunOnFinite ℝ ℝ ι) ↑b.repr
D : Set (ι → ℝ) := Set.pi Set.univ fun x => Set.Ico 0 1
⊢ MeasurableSet (↑f ⁻¹' D)
refine measurableSet_preimage (LinearMap.continuous_of_finiteDimensional f).measurable ?_
no goals
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
this : FiniteDimensional ℝ E
f : E →ₗ[ℝ] ι → ℝ := LinearMap.comp ↑(Finsupp.linearEquivFunOnFinite ℝ ℝ ι) ↑b.repr
D : Set (ι → ℝ) := Set.pi Set.univ fun x => Set.Ico 0 1
⊢ MeasurableSet D
exact MeasurableSet.pi Set.countable_univ fun _ _ => measurableSet_Ico
case h
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
this : FiniteDimensional ℝ E
f : E →ₗ[ℝ] ι → ℝ := LinearMap.comp ↑(Finsupp.linearEquivFunOnFinite ℝ ℝ ι) ↑b.repr
D : Set (ι → ℝ) := Set.pi Set.univ fun x => Set.Ico 0 1
x✝ : E
⊢ x✝ ∈ fundamentalDomain b ↔ x✝ ∈ ↑f ⁻¹' D
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
this : FiniteDimensional ℝ E
f : E →ₗ[ℝ] ι → ℝ := LinearMap.comp ↑(Finsupp.linearEquivFunOnFinite ℝ ℝ ι) ↑b.repr
D : Set (ι → ℝ) := Set.pi Set.univ fun x => Set.Ico 0 1
⊢ fundamentalDomain b = ↑f ⁻¹' D
ext
no goals
case h
E : Type u_1
ι : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
b : Basis ι ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : OpensMeasurableSpace E
inst✝ : Finite ι
this : FiniteDimensional ℝ E
f : E →ₗ[ℝ] ι → ℝ := LinearMap.comp ↑(Finsupp.linearEquivFunOnFinite ℝ ℝ ι) ↑b.repr
D : Set (ι → ℝ) := Set.pi Set.univ fun x => Set.Ico 0 1
x✝ : E
⊢ x✝ ∈ fundamentalDomain b ↔ x✝ ∈ ↑f ⁻¹' D
simp only [fundamentalDomain, Set.mem_setOf_eq, LinearMap.coe_comp,
  LinearEquiv.coe_toLinearMap, Set.mem_preimage, Function.comp_apply, Set.mem_univ_pi,
  Finsupp.linearEquivFunOnFinite_apply]