Discrete MetricSpace/EMetricSpace

Stream: Is there code for X?

[Snir Broshi]

Are there instances of Dist/MetricSpace such that dist x y = if x = y then 0 else 1,
and instances of EDist/EMetricSpace such that edist x y = if x = y then 0 else ∞?
aka the metrics that induce the DiscreteTopology.

The closest I found was docs#DiscreteTopology.metrizableSpace, though I'm not sure it's related (and it's MetrizableSpace rather than MetricSpace).

[Filippo A. E. Nuccio]

(deleted)

[Filippo A. E. Nuccio]

In the context of valuations, we have the notion of being non trivial, which is the closest I can find

https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/Valuation/Basic.html#Valuation.IsNontrivial

[Etienne Marion]

I don't think there is. Here https://github.com/leanprover-community/mathlib4/blob/8f62007a980111b87be592665493301acbb05ea4/Mathlib/Topology/Metrizable/CompletelyMetrizable.lean#L255-L287 it was defined inside the declaration.

[Anatole Dedecker]

Mathematically the closest that we have is docs#DiscreteUniformity, which is equivalent to "the uniform structure is precisely the one coming from one of these discrete distances".

[Snir Broshi]

Thanks for the pointers! How would you go about adding this then?

We can add defs for the MetricSpace & EMetricSpace, but should they also be instances for DiscreteTopology?
Also such instances will create a diamond with docs#MetricSpace.toEMetricSpace, but that's also the case for things like docs#Prod.metricSpaceMax and docs#Prod.emetricSpaceMax so maybe it's okay?
Finally, how can we formalize the notion that DiscreteTopology is induced by the metric?

[Etienne Marion]

You should use MetricSpace.replaceTopology and analogous for uniformity to ensure the induced topology and uniformity are defeq to the discrete ones.

Do you mean to add an instance DiscreteTopology -> MetricSpace? This does not really make sense I think, you don't want to always have a metric space structure when you don't need it.

I am not sure we want this actually. Knowing that the discrete topology is induced by a metric is useful, yes, but is it useful to have a specific metric? Why do you want to add this?

[Yakov Pechersky]

#27664

[Snir Broshi]

Etienne Marion said:

Do you mean to add an instance DiscreteTopology -> MetricSpace? This does not really make sense I think, you don't want to always have a metric space structure when you don't need it.

I am not sure we want this actually. Knowing that the discrete topology is induced by a metric is useful, yes, but is it useful to have a specific metric? Why do you want to add this?

I was thinking maybe if we have a DiscreteMetric class that says a MetricSpace is the discrete one, we can do DiscreteMetric X -> @DiscreteTopology _ (X.toUniformSpace.toTopologicalSpace), but idk.
We can also have def WithDiscreteMetric (X : Type*) := X, an instance MetricSpace (WithDiscreteMetric X), an instance TopologicalSpace (WithDiscreteMetric X) using X.toUniformSpace.toTopologicalSpace, and finally DiscreteTopology (WithDiscreteMetric X).

I think it's weird to have the discrete metric and the discrete topology without some sort of theorem/instance that links them. It'll probably also be useful to someone.

[Snir Broshi]

Yakov Pechersky said:

#27664

Looks good! Do you plan to continue working on it to get it merged?
The EMetricSpace version could probably be in a future PR

[Snir Broshi]

btw what spawned this thread is that I wanted to take a product α × ℝ and get the e-metric

edist (a₁, x₁) (a₂, x₂) = (if a₁ = a₂ then edist x₁ x₂ else ∞)

rather than the supremum of the metrics in each axis, since if e.g. α := ℝ there could be an existing metric on α that'll give a finite value to pairs with a₁ ≠ a₂.

If I give α the discrete e-metric, then the product will be exactly what I'm looking for.