Skip to content

feat(Topology/FiberBundle): continuousAt_symm_prodMk_left#38020

Open
Deicyde wants to merge 6 commits intoleanprover-community:masterfrom
Deicyde:continuous_symm_prodMk_left
Open

feat(Topology/FiberBundle): continuousAt_symm_prodMk_left#38020
Deicyde wants to merge 6 commits intoleanprover-community:masterfrom
Deicyde:continuous_symm_prodMk_left

Conversation

@Deicyde
Copy link
Copy Markdown
Contributor

@Deicyde Deicyde commented Apr 13, 2026 •
edited by grunweg
Loading

API lemma for fiber bundle trivializations. Shows that x => e.symm (x,v) is continuous on its natural domain.

Open in Gitpod

@github-actions github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Apr 13, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Apr 13, 2026

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

@github-actions
Copy link
Copy Markdown

github-actions bot commented Apr 13, 2026 •
edited
Loading

PR summary b43655dfe2

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ continuousAt_symm
+ continuousAt_symm_prodMk_left
+ continuousOn_symm_prodMk_left

You can run this locally as follows 
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

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

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

No changes to technical debt.

You can run this locally as

./scripts/reporting/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).

@github-actions github-actions bot added the t-topology Topological spaces, uniform spaces, metric spaces, filters label Apr 13, 2026
@Deicyde Deicyde marked this pull request as ready for review April 13, 2026 22:24
@grunweg grunweg changed the title Feat(Topology/FiberBundle): continuousAt_symm_prodMk_left feat(Topology/FiberBundle): continuousAt_symm_prodMk_left Apr 15, 2026
@grunweg grunweg self-assigned this Apr 15, 2026
grunweg
grunweg reviewed Apr 15, 2026
View reviewed changes
Comment thread Mathlib/Topology/FiberBundle/Trivialization.lean Outdated
/-- For fixed `v ∈ F`, `x ↦ e.symm (x,v)` is continuous at any point in the base set -/
theorem continuousAt_symm_prodMk_left {b : B} {v : F} (hb : b ∈ e.baseSet) :
ContinuousAt (e.symm ∘ (·, v)) b :=
ContinuousAt.comp (e.continuousOn_symm.continuousAt
Copy link
Copy Markdown
Contributor

@grunweg grunweg Apr 15, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you extract e.continuousAt_symm as a separate lemma? (Topology/Homotopy/Lifting also would use that lemma)

Copy link
Copy Markdown
Contributor Author

@Deicyde Deicyde Apr 16, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Added. Do you want me to try to golf some of the proofs in Topology/Homotopy/Lifting? Or save that for a seperate PR?

grunweg
grunweg reviewed Apr 15, 2026
View reviewed changes
Copy link
Copy Markdown
Contributor

@grunweg grunweg left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for the PR! Looks good; I just have a few minor comments.

Comment thread Mathlib/Topology/FiberBundle/Trivialization.lean Outdated
Comment thread Mathlib/Topology/FiberBundle/Trivialization.lean Outdated
Comment thread Mathlib/Topology/FiberBundle/Trivialization.lean Outdated
Comment thread Mathlib/Topology/FiberBundle/Trivialization.lean Outdated
@grunweg grunweg added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 15, 2026
@Deicyde
Copy link
Copy Markdown
Contributor Author

Deicyde commented Apr 16, 2026

-awaiting-author

@github-actions github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 16, 2026
@Deicyde Deicyde requested a review from grunweg April 16, 2026 04:11
grunweg
grunweg reviewed Apr 16, 2026
View reviewed changes
Comment thread Mathlib/Topology/FiberBundle/Trivialization.lean
@@ -592,6 +592,19 @@ theorem continuousAt_proj (ex : x ∈ e.source) : ContinuousAt proj x :=
theorem continuousOn_proj : ContinuousOn proj e.source :=
continuousOn_of_forall_continuousAt fun _ ↦ e.continuousAt_proj

/-- The inverse of a trivialization is continuous at any point in the target. -/
theorem continuousAt_symm {p : B × F} (hp : p ∈ e.target) : ContinuousAt e.symm p :=
Copy link
Copy Markdown
Contributor

@grunweg grunweg Apr 16, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I was thinking of OpenPartialHomeomorph.continuousAt_symm instead --- that will also apply inside Homotopy/Lifting. (And doing that within this PR is fine with me.)

@grunweg grunweg added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 16, 2026
@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Apr 16, 2026

Almost there!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@grunweg grunweg grunweg left review comments

Assignees

@grunweg grunweg

@PatrickMassot PatrickMassot

Labels

awaiting-author A reviewer has asked the author a question or requested changes. new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-topology Topological spaces, uniform spaces, metric spaces, filters

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@Deicyde @grunweg @PatrickMassot