Skip to content

[Merged by Bors] - feat(Topology): restriction of a QuotientMap#13228

Closed
urkud wants to merge 2 commits intomasterfrom
YK-quotientMap-restr
Closed

[Merged by Bors] - feat(Topology): restriction of a QuotientMap#13228
urkud wants to merge 2 commits intomasterfrom
YK-quotientMap-restr

Conversation

@urkud
Copy link
Copy Markdown
Member

@urkud urkud commented May 26, 2024

... to the preimage of an open set is a quotient map.

Open in Gitpod

@urkud
feat(Topology): restriction of a QuotientMap
8f25b03 
... to the preimage of an open set is a quotient map.
@urkud urkud added awaiting-review t-topology Topological spaces, uniform spaces, metric spaces, filters labels May 26, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 9, 2024

PR summary 0668fd7d31

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ QuotientMap.continuousOn_isOpen_iff
+ QuotientMap.restrictPreimage_isOpen
+ image_val_preimage_restrictPreimage
+ preimage_restrictPreimage
+ restrictPreimage_mk

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

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

jcommelin
jcommelin reviewed Jul 12, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Jul 12, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jul 12, 2024
@urkud
feat(Topology): restriction of a QuotientMap (#13228)
12b4bd7 
... to the preimage of an open set is a quotient map.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 12, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Topology): restriction of a QuotientMap [Merged by Bors] - feat(Topology): restriction of a QuotientMap Jul 12, 2024
@mathlib-bors mathlib-bors bot closed this Jul 12, 2024
@mathlib-bors mathlib-bors bot deleted the YK-quotientMap-restr branch July 12, 2024 14:35
@adomani adomani mentioned this pull request Aug 1, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

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

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@urkud @jcommelin @kim-em