Skip to content

[Merged by Bors] - feat: contMDiffOn_section_of_mem_baseSet#26678

Closed
grunweg wants to merge 2 commits intoleanprover-community:masterfrom
grunweg:contMDiffOn_section_baseset
Closed

[Merged by Bors] - feat: contMDiffOn_section_of_mem_baseSet#26678
grunweg wants to merge 2 commits intoleanprover-community:masterfrom
grunweg:contMDiffOn_section_baseset

Conversation

@grunweg
Copy link
Copy Markdown
Contributor

@grunweg grunweg commented Jul 3, 2025 •
edited
Loading

Smoothness of a section can be determined using any trivialisation, not just the preferred trivialisation at a point.

Part of the path towards geodesics and the Levi-Civita connection.

Co-authored by: @PatrickMassot

Open in Gitpod

@grunweg
feat: contMDiffOn_section_of_mem_baseSet
18bb8df 
Smoothness of a section can be determined using any trivialisation, not
just the preferred trivialisation at a point.

Part of the path towards geodesics and the Levi-Civita connection.
This was referenced Jul 3, 2025
Draft
Closed
@github-actions github-actions bot added the t-differential-geometry Manifolds etc label Jul 3, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 3, 2025 •
edited
Loading

PR summary 7672327e9c

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ Trivialization.contMDiffWithinAt_section
+ contMDiffAt_section_of_mem_baseSet
+ contMDiffOn_section_of_mem_baseSet
+ contMDiffOn_section_of_mem_baseSet₀

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 relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

sgouezel
sgouezel reviewed Jul 3, 2025
View reviewed changes
@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Jul 3, 2025

Thanks, all addressed!

@sgouezel
Copy link
Copy Markdown
Contributor

sgouezel commented Jul 5, 2025

bors r+
Thanks!

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Jul 5, 2025
@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Jul 5, 2025

Thanks for the quick review!

mathlib-bors bot pushed a commit that referenced this pull request Jul 5, 2025
@grunweg
feat: contMDiffOn_section_of_mem_baseSet (#26678)
656089c 
Smoothness of a section can be determined using any trivialisation, not just the preferred trivialisation at a point.

Part of the path towards geodesics and the Levi-Civita connection.

Co-authored by: @PatrickMassot
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 5, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: contMDiffOn_section_of_mem_baseSet [Merged by Bors] - feat: contMDiffOn_section_of_mem_baseSet Jul 5, 2025
@mathlib-bors mathlib-bors bot closed this Jul 5, 2025
@grunweg grunweg deleted the contMDiffOn_section_baseset branch July 5, 2025 22:44
joelriou pushed a commit to joelriou/mathlib4 that referenced this pull request Jul 7, 2025
@grunweg @joelriou
feat: contMDiffOn_section_of_mem_baseSet (leanprover-community#26678)
fa2b9af 
Smoothness of a section can be determined using any trivialisation, not just the preferred trivialisation at a point.

Part of the path towards geodesics and the Levi-Civita connection.

Co-authored by: @PatrickMassot
callesonne pushed a commit to callesonne/mathlib4 that referenced this pull request Jul 24, 2025
@grunweg @callesonne
feat: contMDiffOn_section_of_mem_baseSet (leanprover-community#26678)
53a4680 
Smoothness of a section can be determined using any trivialisation, not just the preferred trivialisation at a point.

Part of the path towards geodesics and the Levi-Civita connection.

Co-authored by: @PatrickMassot
hrmacbeth pushed a commit to szqzs/mathlib4 that referenced this pull request Jul 28, 2025
@grunweg @hrmacbeth
feat: contMDiffOn_section_of_mem_baseSet (leanprover-community#26678)
b14b339 
Smoothness of a section can be determined using any trivialisation, not just the preferred trivialisation at a point.

Part of the path towards geodesics and the Levi-Civita connection.

Co-authored by: @PatrickMassot
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@sgouezel sgouezel sgouezel left review comments

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-differential-geometry Manifolds etc

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@grunweg @sgouezel