feat(MeasureTheory): Add measurability of sum and multiplication for EReal

[LorenzoLuccioli]

Add a section about EReal in the file MeasureTheory.Constructions.BorelSpace.Real.lean with the instances for the measurability of the sum and multiplication between two extended real numbers as well as some lemmas that are needed for the proofs.

---

• depends on: [Merged by Bors] - feat(MeasureTheory): generalize instance ContinuousInv.measurableInv #17082

[github-actions]

PR summary b488a22119

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ instance (priority := 100) ContinuousInv.measurableInv [Inv γ] [ContinuousInv γ] :
+ instance : MeasurableAdd₂ EReal := ⟨EReal.lowerSemicontinuous_add.measurable⟩
+ instance : MeasurableMul₂ EReal := by
+ lowerSemicontinuous_add
+ measurable_from_prod_countable''
+ measurable_of_measurable_real_prod
+ measurable_of_measurable_real_real
- instance (priority := 100) TopologicalGroup.measurableInv [Group γ] [TopologicalGroup γ] :

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(MeasureTheory): generalize instance ContinuousInv.measurableInv #17082
  By Dependent Issues (🤖). Happy coding!