PRs from sphere eversion

Stream: PR reviews

[Michael Rothgang]

I just submitted three PRs with lemmas ready for mathlib. (By no means urgent, but perhaps of interest.)

• partial homeomorphisms #9623
• (open) embeddings #9624
• topological partitions of unity #9635

[Michael Rothgang]

Wohoo, first two were reviewed and merged already. Thanks for the fast reviews!
I filed two more PRs, fresh from the press:

• #9669 a function is ContMDiffAt outside of its tsupport
• #9672 a subset of a charted space is open iff its image in each chart is

[Michael Rothgang]

Current situation with PRs awaiting review:

• #9775 (Lie groups), a few easy lemmas merged
• #9778 (Topology/Support), two short lemmas merged
• #9813 (Topology/LocallyFinite), another short lemma
• #9872 (Topology/Algebra/Order/Compact), one pretty short lemma
• #9874 (easy, renaming lemmas) merged and #9873 (cut-off functions)
• #9810 (HausdorffDistance; 25 lines/three lemmas) is blocked on #9809 (splitting that file)

[Michael Rothgang]

(The previous PRs have all been merged, thanks for the reviews!)

[Michael Rothgang]

New PRs waiting for review (I updated the list above):

• #9982 (normed spaces, easy)
• #10001 (four small lemmas about extended charts)
• #10005 (preparatory clean-up) and #10004 (two lemmas about parametric interval integrals)
• #10015 (partitions of unity)
• #10019 (two small lemmas partitions of unity), blocked on #10020 (easy lemma about LocallyFinite)

[Michael Rothgang]

Thanks for the reviews on the three merged PRs in the meantime.

[Michael Rothgang]

Thanks for the reviews; all of these PRs, and all previous ones have been merged now.

[Michael Rothgang]

New list of PRs:

• #9872 (four week friendly ping)
• #11108 and #11110 (more lemmas about parametric integrals)
• #10977 (germs of smooth functions, part 1)

[Michael Rothgang]

The first three PRs have all been merged (thanks again for the reviews). Here are a few more:

• #11185 (parametric integrals, again)
• #11264 and #11265 (two lemmas about flags of a basis) - each ~10 lines, so a short review
• #11387 (codimension two subspaces have path-connected complement): a prerequisite for the last PR, but purely topological
• #11341 (continuous affine equivalences), a prerequisite for
• #11344 (ample sets in real vector spaces), which allows
• #11342 (complements of codimension two subspaces are ample)

The last two PRs would be the first file outside of ToMathlib being upstreamed this year.

[Michael Rothgang]

Two PRs from this list are basically ready, but require a second pair of eyes:

• @Sébastien Gouëzel took a look #11185 and generalised the code to remove an assumption. This means they cannot approve their own code.
• @Anatole Dedecker approved #11344, but doesn't want to merge since they were also involved in the project. Can somebody who has no "conflict of interest" take a look?

[Michael Rothgang]

#11337 is also ready for a look again. Thank you!