Skip to content

[Merged by Bors] - fix(Topology/Covering): switch to standard definition#24983

Closed
alreadydone wants to merge 8 commits intomasterfrom
IsCoveringMap_fix
Closed

[Merged by Bors] - fix(Topology/Covering): switch to standard definition#24983
alreadydone wants to merge 8 commits intomasterfrom
IsCoveringMap_fix

Conversation

@alreadydone
Copy link
Copy Markdown
Contributor

@alreadydone alreadydone commented May 17, 2025 •
edited
Loading

As discussed in #mathlib4 > edge cases not covered by `IsCoveringMap` @ 💬, the previous definition doesn't include examples like the inclusion of a one-point space into a two-point discrete space.

Open in Gitpod

@alreadydone alreadydone requested a review from tb65536 May 17, 2025 23:00
@alreadydone alreadydone added the t-topology Topological spaces, uniform spaces, metric spaces, filters label May 17, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented May 17, 2025 •
edited
Loading

PR summary ca163bb348

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ continuousOn_proj
+ discreteTopology_fiber
+ fiberHomeomorph
+ of_discreteTopology
+ of_fiber_homeomorph
+ of_preimage_eq_empty
+ of_trivialization
+ toTrivialization'
++ mk'
++ of_isEmpty

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).

tb65536
tb65536 reviewed May 17, 2025
View reviewed changes
@alreadydone alreadydone mentioned this pull request May 18, 2025
Closed
4 tasks
alreadydone
alreadydone commented May 20, 2025
View reviewed changes
@leanprover-community-bot-assistant
Copy link
Copy Markdown
Collaborator

leanprover-community-bot-assistant commented Jun 7, 2025

This pull request has conflicts, please merge master and resolve them.

@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 7, 2025
@alreadydone alreadydone removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 9, 2025
@alreadydone alreadydone mentioned this pull request Jul 8, 2025
Draft
3 tasks
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 9, 2025
@leanprover-community-bot-assistant
Copy link
Copy Markdown
Collaborator

leanprover-community-bot-assistant commented Jul 9, 2025

This pull request has conflicts, please merge master and resolve them.

@alreadydone alreadydone removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 9, 2025
@alreadydone alreadydone mentioned this pull request Jul 9, 2025
Draft
3 tasks
tb65536
tb65536 approved these changes Jul 14, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@tb65536 tb65536 left a comment

Choose a reason for hiding this comment

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

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 14, 2025

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

@ghost ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jul 14, 2025
@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented Jul 15, 2025

Thanks 🎉

bors merge

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Jul 15, 2025
mathlib-bors bot pushed a commit that referenced this pull request Jul 15, 2025
@alreadydone
fix(Topology/Covering): switch to standard definition (#24983)
3d1fc47 
As discussed in [#mathlib4 > edge cases not covered by &#96;IsCoveringMap&#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/edge.20cases.20not.20covered.20by.20.60IsCoveringMap.60/near/518413081), the previous definition doesn't include examples like the inclusion of a one-point space into a two-point discrete space.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 15, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title fix(Topology/Covering): switch to standard definition [Merged by Bors] - fix(Topology/Covering): switch to standard definition Jul 15, 2025
@mathlib-bors mathlib-bors bot closed this Jul 15, 2025
@mathlib-bors mathlib-bors bot deleted the IsCoveringMap_fix branch July 15, 2025 09:22
BeibeiX0 pushed a commit to BeibeiX0/mathlib4 that referenced this pull request Jul 16, 2025
@alreadydone @BeibeiX0
fix(Topology/Covering): switch to standard definition (leanprover-com…
d95f033 
…munity#24983)

As discussed in [#mathlib4 > edge cases not covered by &leanprover-community#96;IsCoveringMap&leanprover-community#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/edge.20cases.20not.20covered.20by.20.60IsCoveringMap.60/near/518413081), the previous definition doesn't include examples like the inclusion of a one-point space into a two-point discrete space.
callesonne pushed a commit to callesonne/mathlib4 that referenced this pull request Jul 24, 2025
@alreadydone @callesonne
fix(Topology/Covering): switch to standard definition (leanprover-com…
43d26ab 
…munity#24983)

As discussed in [#mathlib4 > edge cases not covered by &leanprover-community#96;IsCoveringMap&leanprover-community#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/edge.20cases.20not.20covered.20by.20.60IsCoveringMap.60/near/518413081), the previous definition doesn't include examples like the inclusion of a one-point space into a two-point discrete space.
hrmacbeth pushed a commit to szqzs/mathlib4 that referenced this pull request Jul 28, 2025
@alreadydone @hrmacbeth
fix(Topology/Covering): switch to standard definition (leanprover-com…
2dd65fe 
…munity#24983)

As discussed in [#mathlib4 > edge cases not covered by &leanprover-community#96;IsCoveringMap&leanprover-community#96; @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/edge.20cases.20not.20covered.20by.20.60IsCoveringMap.60/near/518413081), the previous definition doesn't include examples like the inclusion of a one-point space into a two-point discrete space.
@alreadydone alreadydone mentioned this pull request Dec 17, 2025
Closed
1 task
@alreadydone alreadydone moved this from Open to Merged in Covering spaces and étale spaces Mar 6, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@tb65536 tb65536 tb65536 approved these changes

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-topology Topological spaces, uniform spaces, metric spaces, filters

Projects

Covering spaces and étale spaces
Status: Merged

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@alreadydone @leanprover-community-bot-assistant @jcommelin @tb65536