mathlib

e1a7bdeb - refactor(topology/*): add `uniform_space.of_fun`, use it (#18495)

refactor(topology/*): add `uniform_space.of_fun`, use it (#18495) * 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`.