Skip to content

[Merged by Bors] - feat: define RestrictGenTopology#13452

Closed
urkud wants to merge 16 commits intomasterfrom
YK-topgenfam
Closed

[Merged by Bors] - feat: define RestrictGenTopology#13452
urkud wants to merge 16 commits intomasterfrom
YK-topgenfam

Conversation

@urkud
Copy link
Copy Markdown
Member

@urkud urkud commented Jun 1, 2024

Open in Gitpod

@urkud urkud added the t-topology Topological spaces, uniform spaces, metric spaces, filters label Jun 1, 2024
urkud
urkud commented Jun 2, 2024
View reviewed changes
@urkud urkud marked this pull request as ready for review June 2, 2024 16:40
@urkud urkud requested a review from ADedecker June 2, 2024 16:40
@urkud urkud mentioned this pull request Jun 2, 2024
Closed
2 tasks
@ADedecker ADedecker mentioned this pull request Jun 11, 2024
Closed
@dupuisf
Copy link
Copy Markdown
Contributor

dupuisf commented Jun 29, 2024

Looks good!

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 29, 2024

✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@github-actions github-actions bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Jun 29, 2024
dupuisf
dupuisf reviewed Jun 29, 2024
View reviewed changes
@urkud urkud added the auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. label Jun 29, 2024
@github-actions
Copy link
Copy Markdown

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

PR summary 95ca0fbb8e

Import changes

Dependency changes

File Base Count Head Count Change
Mathlib.Topology.UniformSpace.UniformConvergenceTopology 685 687 +2 (+0.29%)

Declarations diff

+ RestrictGenTopology
+ continuous_iff
+ enlarge
+ instance _root_.instTopologicalSpaceSubtype {p : X → Prop} [t : TopologicalSpace X] :
+ isClosed_iff
+ isClosed_setOf_continuous
+ isCompact_of_seq
+ isOpen_iff
+ mono
+ of_continuous_prop
+ of_isClosed
+ of_seq
- instTopologicalSpaceSubtype

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>

@ghost
Copy link
Copy Markdown

ghost commented Jun 29, 2024

As this PR is labelled auto-merge-after-CI, we are now sending it to bors:

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Jun 29, 2024
@urkud
feat: define RestrictGenTopology (#13452)
0b163fd
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 29, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: define RestrictGenTopology [Merged by Bors] - feat: define RestrictGenTopology Jun 29, 2024
@mathlib-bors mathlib-bors bot closed this Jun 29, 2024
@mathlib-bors mathlib-bors bot deleted the YK-topgenfam branch June 29, 2024 23:08
dagurtomas pushed a commit that referenced this pull request Jul 2, 2024
@urkud @dagurtomas
feat: define RestrictGenTopology (#13452)
7e34134
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@dupuisf dupuisf dupuisf left review comments

@ADedecker ADedecker Awaiting requested review from ADedecker

Assignees

No one assigned

Labels

auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). 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

@urkud @dupuisf