Skip to content

[Merged by Bors] - feat: (𝓝[<] x).NeBot instances for Prod, Pi, OrderDual#13642

Closed
YaelDillies wants to merge 2 commits intomasterfrom
nhds_within_iio_ne_bot
Closed

[Merged by Bors] - feat: (𝓝[<] x).NeBot instances for Prod, Pi, OrderDual#13642
YaelDillies wants to merge 2 commits intomasterfrom
nhds_within_iio_ne_bot

Conversation

@YaelDillies
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies commented Jun 8, 2024

Open in Gitpod

@YaelDillies YaelDillies added awaiting-review t-topology Topological spaces, uniform spaces, metric spaces, filters t-order Order theory labels Jun 8, 2024
@github-actions
Copy link
Copy Markdown

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

PR summary

Import changes

No significant changes to the import graph

Declarations diff

+ OrderDual.instDiscreteTopology
+ OrderDual.instNeBotNhdsWithinIio
+ OrderDual.instNeBotNhdsWithinIoi
+ OrderDual.instTopologicalSpace
+ Pi.instNeBotNhdsWithinIio
+ Pi.instNeBotNhdsWithinIoi
+ Prod.instNeBotNhdsWithinIio
+ Prod.instNeBotNhdsWithinIoi
+ eval_image_pi_of_not_mem
+ isOpenMap_eval
+ lt_of_le_of_lt
+ lt_of_lt_of_le
+ mk_lt_mk_of_le_of_lt
+ mk_lt_mk_of_lt_of_le
+ nhdsWithin_neBot
- instance : TopologicalSpace Xᵒᵈ
- instance [DiscreteTopology X] : DiscreteTopology Xᵒᵈ

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>

@YaelDillies YaelDillies mentioned this pull request Jun 8, 2024
Closed
1 task
urkud
urkud reviewed Jun 9, 2024
View reviewed changes
Ruben-VandeVelde
Ruben-VandeVelde approved these changes Jun 16, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@Ruben-VandeVelde Ruben-VandeVelde 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 Jun 16, 2024

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jun 16, 2024
@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Jun 17, 2024

Thanks!

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jun 17, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jun 17, 2024
@YaelDillies
feat: (𝓝[<] x).NeBot instances for Prod, Pi, OrderDual (#13642)
217718f
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 17, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: (𝓝[<] x).NeBot instances for Prod, Pi, OrderDual [Merged by Bors] - feat: (𝓝[<] x).NeBot instances for Prod, Pi, OrderDual Jun 17, 2024
@mathlib-bors mathlib-bors bot closed this Jun 17, 2024
@mathlib-bors mathlib-bors bot deleted the nhds_within_iio_ne_bot branch June 17, 2024 11:20
AntoineChambert-Loir pushed a commit that referenced this pull request Jun 20, 2024
@YaelDillies @AntoineChambert-Loir
feat: (𝓝[<] x).NeBot instances for Prod, Pi, OrderDual (#13642)
4201a43
kbuzzard pushed a commit that referenced this pull request Jun 26, 2024
@YaelDillies @kbuzzard
feat: (𝓝[<] x).NeBot instances for Prod, Pi, OrderDual (#13642)
031ac5c
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@urkud urkud urkud left review comments

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde approved these changes

Assignees

No one assigned

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. ready-to-merge This PR has been sent to bors. t-order Order theory 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.

4 participants

@YaelDillies @riccardobrasca @urkud @Ruben-VandeVelde