[Merged by Bors] - chore(AEEqOfIntegral): weaken TC assumptions in 2 lemmas

[urkud]

.. from T2Space to R1Space

---

[github-actions]

PR summary d8289fddcd

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ iUnion_closure_compactCovering

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>

[grunweg]

Thanks, looks good. (I have to look this up as I didn't see R1 spaces before: a T2 space is R1, so this is a real generalisation.)maintainer merge

[grunweg]

Now with proper formatting
maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by grunweg.

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style