metrizability

Stream: maths

[Yury G. Kudryashov]

I have a proof of the following theorem:

import topology.metric_space.basic

open set function metric list filter
open_locale nnreal filter uniformity

protected lemma uniform_space.metrizable_uniformity (X : Type*) [uniform_space X]
  [is_countably_generated (𝓤 X)] :
  ∃ I : pseudo_metric_space X, I.to_uniform_space = ‹_› :=

It says that any uniform_space structure with countably generated uniformity filter is (pseudo)metrizable. I want to add an instance saying that a uniform space with countably generated uniformity filter is metrizable, then replace [uniform_space X] [is_countably_generated (𝓤 X)] with [metrizable_space X] here and there (namely, in all lemmas that don't use uniformity structure in their statements). However, docs#topological_space.metrizable_space deals with docs#metric_space, not docs#pseudo_metric_space.

@Sebastien Gouezel What do you think about replacing metrizable_space with pseudo_metrizable_space and adding [t?_space] assumption (I guess, t0_space is enough) to lemmas that don't work in pseudo metric spaces?

[Sebastien Gouezel]

I'd rather keep the metrizable_space typeclass as it shows up a lot in many statements on integration. But we can definitely add another pseudo_metrizable_space typeclass (and add an instance from the former to the latter).

[Yury G. Kudryashov]

BTW, what is the verb for metrizable? I want to add a tactic similar to tactic#borelize that adds a (pseudo_)metric_space instance that agrees with an existing uniform_space or topological_space structure.

[Sebastien Gouezel]

I'm not sure borelize is a real word either. The opinion of a native speaker would be much more useful, but I'd probably go for metrize.

[Eric Wieser]

metrize or metrify or metricify would be my choices (I'm a native speaker)

[Yury G. Kudryashov]

I add a definition in #14053

[Jireh Loreaux]

metrize and metrify (but not metricify) sounded almost equally good to me (also a native speaker), so I did some reading. Turns out this is one of the rare cases where both suffixes are acceptable: "you can do it either way with words stressed on the next-to-last syllable that end in unstressed /i/. But they're the only ones."

I think I have a slight preference for metrize for the parallelism with metrizable.

[Yury G. Kudryashov]

@Sebastien Gouezel I'm running into the following problem with metrizable. I have a lemma in #14052 saying that a uniform_space structure with a countably generated uniformity filter is pseudo-metrizable. It is natural to use this lemma to add instances uniform_space X → is_countably_generated (𝓤 X) → pseudo_metrizable_space X and uniform_space X → is_countably_generated (𝓤 X) → t0_space X → metrizable_space X but the latter instance leads to a cycle.

[Yury G. Kudryashov]

OTOH, if I drop class metrizable_space, then Lean can't deduce t2_space X from [pseudo_metrizable_space X] [t0_space X].

[Yury G. Kudryashov]

So, we need to use lemma, not instance for one of the implications (at least till Lean 4). Which one?

[Sebastien Gouezel]

I'd drop the latter one.

[Yury G. Kudryashov]

uniform_space X → is_countably_generated (𝓤 X) → t0_space X → metrizable_space X?

[Sebastien Gouezel]

Yes.