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(topology/*): add uniform_space.of_fun
, use it
#18495
Conversation
uniform_space.core.of_fun
, use ituniform_space.of_fun
, use it
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.
Looks good, but could someone who has used uniform spaces (@sgouezel, maybe?) check?
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.
Thanks 🎉
bors merge
* Fix `simps` config for `absolute_value`. * Define `uniform_space.of_fun` and use it for `absolute_value.uniform_space`, `pseudo_emetric_space`, and `pseudo_metric_space`. * Add `filter.tendsto_infi_infi` and `filter.tendsto_supr_supr`. * Rename `pseudo_metric_space.of_metrizable` and `metric_space.of_metrizable` to `*.of_dist_topology`. * Add `metric.to_uniform_space_eq` and `metric.uniformity_basis_dist_rat`. * Migrate `topology.uniform_space.absolute_value` to bundled `absolute_value`.
Build failed: |
bors merge |
* Fix `simps` config for `absolute_value`. * Define `uniform_space.of_fun` and use it for `absolute_value.uniform_space`, `pseudo_emetric_space`, and `pseudo_metric_space`. * Add `filter.tendsto_infi_infi` and `filter.tendsto_supr_supr`. * Rename `pseudo_metric_space.of_metrizable` and `metric_space.of_metrizable` to `*.of_dist_topology`. * Add `metric.to_uniform_space_eq` and `metric.uniformity_basis_dist_rat`. * Migrate `topology.uniform_space.absolute_value` to bundled `absolute_value`.
Build failed: |
bors merge |
* Fix `simps` config for `absolute_value`. * Define `uniform_space.of_fun` and use it for `absolute_value.uniform_space`, `pseudo_emetric_space`, and `pseudo_metric_space`. * Add `filter.tendsto_infi_infi` and `filter.tendsto_supr_supr`. * Rename `pseudo_metric_space.of_metrizable` and `metric_space.of_metrizable` to `*.of_dist_topology`. * Add `metric.to_uniform_space_eq` and `metric.uniformity_basis_dist_rat`. * Migrate `topology.uniform_space.absolute_value` to bundled `absolute_value`.
Pull request successfully merged into master. Build succeeded: |
uniform_space.of_fun
, use ituniform_space.of_fun
, use it
simps
config forabsolute_value
.uniform_space.of_fun
and use it forabsolute_value.uniform_space
,pseudo_emetric_space
, andpseudo_metric_space
.filter.tendsto_infi_infi
andfilter.tendsto_supr_supr
.pseudo_metric_space.of_metrizable
andmetric_space.of_metrizable
to*.of_dist_topology
.metric.to_uniform_space_eq
andmetric.uniformity_basis_dist_rat
.topology.uniform_space.absolute_value
to bundledabsolute_value
.Most of the changes to the already ported files are backported from mathlib4 (or a pending PR to mathlib4). I'll sync the rest the day after this PR is merged.