Skip to content

[Merged by Bors] - chore(Topology): miscellaneous renames#18398

Closed
YaelDillies wants to merge 4 commits intomasterfrom
topology_misc_renames
Closed

[Merged by Bors] - chore(Topology): miscellaneous renames#18398
YaelDillies wants to merge 4 commits intomasterfrom
topology_misc_renames

Conversation

@YaelDillies
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies commented Oct 29, 2024

A bunch of lemma name improvements that were missed in the prerequisites to #15993

Open in Gitpod

@YaelDillies YaelDillies added the t-topology Topological spaces, uniform spaces, metric spaces, filters label Oct 29, 2024
@YaelDillies YaelDillies mentioned this pull request Oct 29, 2024
Closed
11 tasks
@github-actions
Copy link
Copy Markdown

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

PR summary cc6541b619

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ IsClosedEmbedding.inl
+ IsClosedEmbedding.inr
+ IsClosedEmbedding.sigmaMk
+ IsClosedEmbedding.uliftDown
+ IsOpenEmbedding.inl
+ IsOpenEmbedding.inr
+ IsOpenEmbedding.isOpen_iff_image_isOpen
+ IsOpenEmbedding.isOpen_iff_preimage_isOpen
+ IsOpenEmbedding.of_continuous_injective_isOpenMap
+ IsOpenEmbedding.sigmaMk
+ IsUniformEmbedding.isClosedEmbedding
+ _root_.openEmbedding_id
+ instance : CompactSpace (Aut F) := (autEmbedding_isClosedEmbedding F).compactSpace
+ isClosed_iff_image_isClosed
+ isClosed_iff_preimage_isClosed
+ isDenseInducing
+ isOpenEmbedding_iff_continuous_injective_isOpenMap
+ isOpenEmbedding_of_pullback
+ isOpenEmbedding_sigmaMap
+ of_continuous_injective_isClosedMap
++ id
- _root_.IsClosedEmbedding.of_continuous_injective_isClosedMap
- _root_.isClosedEmbedding_id
- instance : CompactSpace (Aut F) := IsClosedEmbedding.compactSpace (autEmbedding_isClosedEmbedding F)
- isOpenEmbedding_id
- isOpenEmbedding_of_continuous_injective_open
- openEmbedding_id

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.

@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 Oct 30, 2024
@YaelDillies YaelDillies force-pushed the topology_misc_renames branch from b55d3f5 to 07b1b63 Compare October 30, 2024 08:46
@YaelDillies YaelDillies force-pushed the topology_misc_renames branch from 07b1b63 to fb6930f Compare October 30, 2024 08:56
@YaelDillies YaelDillies removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 30, 2024
b-mehta
b-mehta approved these changes Nov 5, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@b-mehta b-mehta left a comment

Choose a reason for hiding this comment

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

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Nov 5, 2024
mathlib-bors bot pushed a commit that referenced this pull request Nov 5, 2024
@YaelDillies
chore(Topology): miscellaneous renames (#18398)
808d429 
A bunch of lemma name improvements that were missed in the prerequisites to #15993
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 5, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(Topology): miscellaneous renames [Merged by Bors] - chore(Topology): miscellaneous renames Nov 5, 2024
@mathlib-bors mathlib-bors bot closed this Nov 5, 2024
@mathlib-bors mathlib-bors bot deleted the topology_misc_renames branch November 5, 2024 14:13
TobiasLeichtfried pushed a commit that referenced this pull request Nov 21, 2024
@YaelDillies @TobiasLeichtfried
chore(Topology): miscellaneous renames (#18398)
2cffdf2 
A bunch of lemma name improvements that were missed in the prerequisites to #15993
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@b-mehta b-mehta b-mehta 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

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@YaelDillies @b-mehta @leanprover-community-bot-assistant