Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(topology/metric_space/hausdorff_distance): A cthickening is an intersection of thickenings#17258

Closed
YaelDillies wants to merge 1 commit intomasterfrom
cthickening_eq_Inter_thickening''
Closed

[Merged by Bors] - feat(topology/metric_space/hausdorff_distance): A cthickening is an intersection of thickenings#17258
YaelDillies wants to merge 1 commit intomasterfrom
cthickening_eq_Inter_thickening''

Conversation

@YaelDillies
Copy link
Copy Markdown
Collaborator

... unconditionally. This is useful for me because being an upper set is a property that holds under unions, regardless of whether 0 ≤ δ or not.


Open in Gitpod

@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR easy < 20s of review time. See the lifecycle page for guidelines. t-topology Topological spaces, uniform spaces, metric spaces, filters labels Oct 30, 2022
@sgouezel
Copy link
Copy Markdown
Collaborator

sgouezel commented Nov 7, 2022

bors r+

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Nov 7, 2022
bors bot pushed a commit that referenced this pull request Nov 7, 2022
… intersection of `thickenings` (#17258)

... unconditionally. This is useful for me because being an upper set is a property that holds under unions, regardless of whether `0 ≤ δ` or not.
@bors
Copy link
Copy Markdown

bors bot commented Nov 8, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(topology/metric_space/hausdorff_distance): A cthickening is an intersection of thickenings [Merged by Bors] - feat(topology/metric_space/hausdorff_distance): A cthickening is an intersection of thickenings Nov 8, 2022
@bors bors bot closed this Nov 8, 2022
@bors bors bot deleted the cthickening_eq_Inter_thickening'' branch November 8, 2022 01:00
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Labels

easy < 20s of review time. See the lifecycle page for guidelines. ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) t-topology Topological spaces, uniform spaces, metric spaces, filters

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants