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.
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
[Merged by Bors] - refactor(UniformSpace): change the definition #10901
Conversation
We had duplicated API between topological spaces and uniform spaces. In this PR I mostly deduplicate it with some exceptions: - `SeparationQuotient.lift'` and `SeparationQuotient.map` are leftovers from the old version that are designed to work with uniform spaces; - probably, some theorems/instances still assume `UniformSpace` when `TopologicalSpace` would work.
This is an abbreviation for `Filter.lim` that deduces `Nonempty` from `Cauchy`. Use it to drop unneeded `Nonempty`/`Inhabited` assumptions.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
bors d+
Thanks for doing this!
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
- replace `isOpen_uniformity` with `nhds_eq_comap_uniformity` as I suggested in #2028 - don't extend `UniformSpace.Core` so that we can drop `refl`, as it follows from `nhds_eq_comap_uniformity`; - drop `UniformSpace.mk'` - can't be a `match_pattern` anymore; - deprecate `UniformSpace.ofNhdsEqComap`.
Build failed (retrying...): |
- replace `isOpen_uniformity` with `nhds_eq_comap_uniformity` as I suggested in #2028 - don't extend `UniformSpace.Core` so that we can drop `refl`, as it follows from `nhds_eq_comap_uniformity`; - drop `UniformSpace.mk'` - can't be a `match_pattern` anymore; - deprecate `UniformSpace.ofNhdsEqComap`.
Build failed: |
bors merge |
- replace `isOpen_uniformity` with `nhds_eq_comap_uniformity` as I suggested in #2028 - don't extend `UniformSpace.Core` so that we can drop `refl`, as it follows from `nhds_eq_comap_uniformity`; - drop `UniformSpace.mk'` - can't be a `match_pattern` anymore; - deprecate `UniformSpace.ofNhdsEqComap`.
Pull request successfully merged into master. Build succeeded: |
- replace `isOpen_uniformity` with `nhds_eq_comap_uniformity` as I suggested in #2028 - don't extend `UniformSpace.Core` so that we can drop `refl`, as it follows from `nhds_eq_comap_uniformity`; - drop `UniformSpace.mk'` - can't be a `match_pattern` anymore; - deprecate `UniformSpace.ofNhdsEqComap`.
- replace `isOpen_uniformity` with `nhds_eq_comap_uniformity` as I suggested in #2028 - don't extend `UniformSpace.Core` so that we can drop `refl`, as it follows from `nhds_eq_comap_uniformity`; - drop `UniformSpace.mk'` - can't be a `match_pattern` anymore; - deprecate `UniformSpace.ofNhdsEqComap`.
- replace `isOpen_uniformity` with `nhds_eq_comap_uniformity` as I suggested in #2028 - don't extend `UniformSpace.Core` so that we can drop `refl`, as it follows from `nhds_eq_comap_uniformity`; - drop `UniformSpace.mk'` - can't be a `match_pattern` anymore; - deprecate `UniformSpace.ofNhdsEqComap`.
- replace `isOpen_uniformity` with `nhds_eq_comap_uniformity` as I suggested in #2028 - don't extend `UniformSpace.Core` so that we can drop `refl`, as it follows from `nhds_eq_comap_uniformity`; - drop `UniformSpace.mk'` - can't be a `match_pattern` anymore; - deprecate `UniformSpace.ofNhdsEqComap`.
- replace `isOpen_uniformity` with `nhds_eq_comap_uniformity` as I suggested in #2028 - don't extend `UniformSpace.Core` so that we can drop `refl`, as it follows from `nhds_eq_comap_uniformity`; - drop `UniformSpace.mk'` - can't be a `match_pattern` anymore; - deprecate `UniformSpace.ofNhdsEqComap`.
- replace `isOpen_uniformity` with `nhds_eq_comap_uniformity` as I suggested in #2028 - don't extend `UniformSpace.Core` so that we can drop `refl`, as it follows from `nhds_eq_comap_uniformity`; - drop `UniformSpace.mk'` - can't be a `match_pattern` anymore; - deprecate `UniformSpace.ofNhdsEqComap`.
isOpen_uniformity
withnhds_eq_comap_uniformity
as I suggested in refactor: redefine
UniformSpace
#2028UniformSpace.Core
so that we can droprefl
,as it follows from
nhds_eq_comap_uniformity
;UniformSpace.mk'
- can't be amatch_pattern
anymore;UniformSpace.ofNhdsEqComap
.separationRel
#10644UniformOnFun
#10873