We prove some lemmas that will be useful in following PRs #6832 and #7037, mainly:
```lean
theorem Basis.addHaar_eq {b : Basis ι ℝ E} {b' : Basis ι' ℝ E} :
     b.addHaar = b'.addHaar ↔ b.addHaar b'.parallelepiped = 1

theorem Basis.parallelepiped_eq_map (b : Basis ι ℝ E) :
     b.parallelepiped = (TopologicalSpace.PositiveCompacts.piIcc01 ι).map b.equivFun.symm
       b.equivFunL.symm.continuous

theorem Basis.addHaar_map (b : Basis ι ℝ E) (f : E ≃L[ℝ] F) :
    map f b.addHaar = (b.map f.toLinearEquiv).addHaar
```

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

We prove some lemmas that will be useful in following PRs #6832 and #7037, mainly:
```lean
theorem Basis.addHaar_eq {b : Basis ι ℝ E} {b' : Basis ι' ℝ E} :
     b.addHaar = b'.addHaar ↔ b.addHaar b'.parallelepiped = 1

theorem Basis.parallelepiped_eq_map (b : Basis ι ℝ E) :
     b.parallelepiped = (TopologicalSpace.PositiveCompacts.piIcc01 ι).map b.equivFun.symm
       b.equivFunL.symm.continuous

theorem Basis.addHaar_map (b : Basis ι ℝ E) (f : E ≃L[ℝ] F) :
    map f b.addHaar = (b.map f.toLinearEquiv).addHaar
```

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

…nd ι → ℝ is volume preserving (#7037)

We prove that the two `MeasureSpace` structures on $\mathbb{R}^\iota$, the one coming from its identification with `ι→ ℝ` and the one coming from `EuclideanSpace ℝ ι`, agree in the sense that the measure equivalence between the two corresponding volumes is measure preserving. 


Co-authored-by: Eric Wieser <wieser.eric@gmail.com>



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

We prove some lemmas that will be useful in following PRs #6832 and #7037, mainly:
```lean
theorem Basis.addHaar_eq {b : Basis ι ℝ E} {b' : Basis ι' ℝ E} :
     b.addHaar = b'.addHaar ↔ b.addHaar b'.parallelepiped = 1

theorem Basis.parallelepiped_eq_map (b : Basis ι ℝ E) :
     b.parallelepiped = (TopologicalSpace.PositiveCompacts.piIcc01 ι).map b.equivFun.symm
       b.equivFunL.symm.continuous

theorem Basis.addHaar_map (b : Basis ι ℝ E) (f : E ≃L[ℝ] F) :
    map f b.addHaar = (b.map f.toLinearEquiv).addHaar
```

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

…nd ι → ℝ is volume preserving (#7037)

We prove that the two `MeasureSpace` structures on $\mathbb{R}^\iota$, the one coming from its identification with `ι→ ℝ` and the one coming from `EuclideanSpace ℝ ι`, agree in the sense that the measure equivalence between the two corresponding volumes is measure preserving. 


Co-authored-by: Eric Wieser <wieser.eric@gmail.com>



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>