feat: immersions are locally embeddings#28905
feat: immersions are locally embeddings#28905grunweg wants to merge 40 commits intoleanprover-community:masterfrom
Conversation
PR summary 54bd5cb866
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Geometry.Manifold.Immersion | 1964 | 1971 | +7 (+0.36%) |
| Mathlib.Geometry.Manifold.ContMDiff.Atlas | 1954 | 1957 | +3 (+0.15%) |
Import changes for all files
| Files | Import difference |
|---|---|
Mathlib.Geometry.Manifold.ContMDiff.Atlas |
3 |
Mathlib.Geometry.Manifold.Immersion |
7 |
Declarations diff
+ ContDiffWithinAt.fst
+ ContDiffWithinAt.snd
+ IsEmbedding.subtype_map_of_subset
+ _root_.Topology.IsEmbedding.comp_restrict
+ contDiffAt_prod_iff
+ contDiffOn_prod_iff
+ contDiffWithinAt_prod_iff
+ contDiff_prod_iff
+ contMDiffOn_extend
+ contMDiffOn_writtenInExtend_iff
+ contMDiffWithinAt_writtenInExtend_iff
+ eqOn_domChart_source
+ extend_target_eq_image_source
+ isClosedEmbedding_symm_restrict
+ isEmbedding_extend_restrict
+ isEmbedding_extend_symm_restrict
+ isEmbedding_restr_domChart_source
+ isEmbedding_symm_restrict
+ rightInverse_restrict
++ contMDiffAt
++ continuousAt
++ exists_nbhd_restr_isEmbedding
++ mapsto_domChart_source_codChart_source
+++ contMDiff
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.
No changes to technical debt.
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
|
This PR/issue depends on: |
fcc5d4d to
8e35b1c
Compare
|
This pull request has conflicts, please merge |
Use I and J consistently. Also add further variables for use when adding products.
There are a bunch of CI warnings, which are all false positives.
Co-authored-by: Christian Merten <christian@merten.dev>
This reverts commit 1b7b2e0.
Co-authored-by: Christian Merten <christian@merten.dev>
With an AI attempt as a starting point; cleaned up by me.
abf0809 to
28ba7ba
Compare
|
This pull request has conflicts, please merge |
Hopefully, this can be used for the topological portion of #28865. (That part is not certain yet, the rest works.)
Needs some clean-up in both the immersions file, and need to move the helper results about embeddings to the correct location.