Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat: nhdsSet sends intersection of compact sets to their infimum #11869

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - feat: nhdsSet sends intersection of compact sets to their infimum #11869

wants to merge 3 commits into from

Conversation

ADedecker
Copy link
Member

Open in Gitpod

@ADedecker ADedecker added awaiting-review awaiting-CI t-topology Topological spaces, uniform spaces, metric spaces, filters labels Apr 3, 2024
@ocfnash
Copy link
Contributor

ocfnash commented Apr 3, 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 Apr 3, 2024
mathlib-bors bot pushed a commit that referenced this pull request Apr 3, 2024
@ADedecker
feat: nhdsSet sends intersection of compact sets to their infimum (#1…
fcf9a43 
…1869)
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Apr 4, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: nhdsSet sends intersection of compact sets to their infimum [Merged by Bors] - feat: nhdsSet sends intersection of compact sets to their infimum Apr 4, 2024
@mathlib-bors mathlib-bors bot closed this Apr 4, 2024
@mathlib-bors mathlib-bors bot deleted the AD_compact_test branch April 4, 2024 00:16
ADedecker added a commit that referenced this pull request Apr 4, 2024
@ADedecker
doc: fix typo introduced in #11869
eb4e5cd
mathlib-bors bot pushed a commit that referenced this pull request Apr 4, 2024
@ADedecker
doc: fix typo introduced in #11869 (#11889)
f113278
Louddy pushed a commit that referenced this pull request Apr 15, 2024
@ADedecker @Louddy
feat: nhdsSet sends intersection of compact sets to their infimum (#1…
6fb04de 
…1869)
Louddy pushed a commit that referenced this pull request Apr 15, 2024
@ADedecker @Louddy
doc: fix typo introduced in #11869 (#11889)
f513ef5
atarnoam pushed a commit that referenced this pull request Apr 16, 2024
@ADedecker @atarnoam
feat: nhdsSet sends intersection of compact sets to their infimum (#1…
84dec5e 
…1869)
atarnoam pushed a commit that referenced this pull request Apr 16, 2024
@ADedecker @atarnoam
doc: fix typo introduced in #11869 (#11889)
0647d48
uniwuni pushed a commit that referenced this pull request Apr 19, 2024
@ADedecker @uniwuni
feat: nhdsSet sends intersection of compact sets to their infimum (#1…
435d053 
…1869)
uniwuni pushed a commit that referenced this pull request Apr 19, 2024
@ADedecker @uniwuni
doc: fix typo introduced in #11869 (#11889)
7117d21
callesonne pushed a commit that referenced this pull request Apr 22, 2024
@ADedecker @callesonne
feat: nhdsSet sends intersection of compact sets to their infimum (#1…
74e499c 
…1869)
callesonne pushed a commit that referenced this pull request Apr 22, 2024
@ADedecker @callesonne
doc: fix typo introduced in #11869 (#11889)
97ecfcb
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
@ADedecker @ocfnash