Skip to content

[Merged by Bors] - chore: Rename QuotientMap to IsQuotientMap#18062

Closed
YaelDillies wants to merge 4 commits intomasterfrom
rename_quotient_map
Closed

[Merged by Bors] - chore: Rename QuotientMap to IsQuotientMap#18062
YaelDillies wants to merge 4 commits intomasterfrom
rename_quotient_map

Conversation

@YaelDillies
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies commented Oct 22, 2024 •
edited by kim-em
Loading

Function.Embedding is a type while Embedding is a proposition, and there are many other kinds of embeddings than topological embeddings. Hence this PR is a step towards

  1. renaming Embedding to IsEmbedding and similarly for neighboring declarations (which QuotientMap is)
  2. namespacing it inside Topology

Open in Gitpod

@YaelDillies YaelDillies added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-topology Topological spaces, uniform spaces, metric spaces, filters labels Oct 22, 2024
@YaelDillies YaelDillies mentioned this pull request Oct 22, 2024
Closed
11 tasks
@github-actions
Copy link
Copy Markdown

github-actions bot commented Oct 22, 2024 •
edited
Loading

PR summary d0d22b0027

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ IsQuotientMap
+ IsQuotientMap.continuousOn_isOpen_iff
+ IsQuotientMap.continuous_lift_prod_left
+ IsQuotientMap.continuous_lift_prod_right
+ IsQuotientMap.image_connectedComponent
+ IsQuotientMap.isClopen_preimage
+ IsQuotientMap.of_surjective_continuous
+ IsQuotientMap.preimage_connectedComponent
+ IsQuotientMap.restrictPreimage_isOpen
+ IsQuotientMap.sequentialSpace
+ IsTopologicalBasis.isQuotientMap
+ QuotientRing.isQuotientMap_coe_coe
+ _root_.IsQuotientMap.secondCountableTopology
+ _root_.IsQuotientMap.separableSpace
+ effectiveEpi_iff_isQuotientMap
+ iff_isOpenMap_isQuotientMap
+ isQuotientMap_coe
+ isQuotientMap_fst
+ isQuotientMap_iff
+ isQuotientMap_iff_closed
+ isQuotientMap_im
+ isQuotientMap_mk_symm
+ isQuotientMap_prodMap_mk
+ isQuotientMap_projIcc
+ isQuotientMap_quot_mk
+ isQuotientMap_quotient_mk'
+ isQuotientMap_re
+ isQuotientMap_snd
+ of_comp
+ of_isOpenMap_isQuotientMap
+ proj_isQuotientMap
++ isQuotientMap_proj
+++ isQuotientMap_mk
+++++++ isQuotientMap
+++++----- quotientMap
+++--- quotientMap_mk
++-- quotientMap_proj
++-- to_quotientMap

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.

@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Oct 22, 2024
@YaelDillies
chore: Rename QuotientMap to IsQuotientMap
2f27e1f 
`Function.Embedding` is a type while `Embedding` is a proposition, and there are many other kinds of embeddings than topological embeddings. Hence this PR is a step towards
1. renaming `Embedding` to `IsEmbedding` and similarly for neighboring declarations (which `QuotientMap` is)
2. namespacing it inside `Topology`
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Oct 23, 2024

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Oct 23, 2024
mathlib-bors bot pushed a commit that referenced this pull request Oct 23, 2024
@YaelDillies
chore: Rename QuotientMap to IsQuotientMap (#18062)
1deca17 
`Function.Embedding` is a type while `Embedding` is a proposition, and there are many other kinds of embeddings than topological embeddings. Hence this PR is a step towards
1. renaming `Embedding` to `IsEmbedding` and similarly for neighboring declarations (which `QuotientMap` is)
2. namespacing it inside `Topology`
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 23, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: Rename QuotientMap to IsQuotientMap [Merged by Bors] - chore: Rename QuotientMap to IsQuotientMap Oct 23, 2024
@mathlib-bors mathlib-bors bot closed this Oct 23, 2024
@mathlib-bors mathlib-bors bot deleted the rename_quotient_map branch October 23, 2024 03:17
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

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.

2 participants

@YaelDillies @kim-em