metric_space (fin n)

Stream: maths

[Daniel Roca González]

Hi,

is there some reason against making docs#fin a metric space, with the distance inherited from nat? If simply nobody thought about that I would make a PR.

[Kevin Buzzard]

I can imagine that people might want a finite discrete metric space with n elements for which d(a,b)=1 if a!=b. So maybe you could make it but make it a def instead of an instance?

[Reid Barton]

I had the same first reaction but upon reflection I'm not sure how pertinent it is, because you could equally well want to put this 0-1 metric on an arbitrary type.

[Daniel Roca González]

Is there a way to "remove" an instance?

[Yaël Dillies]

local attribute [-instance] your_instance

[Yaël Dillies]

Reid Barton said:

I had the same first reaction but upon reflection I'm not sure how pertinent it is, because you could equally well want to put this 0-1 metric on an arbitrary type.

This calls for a discrete_metric type synonym, I suppose.

[Daniel Roca González]

Also different question but related: if we have an injective function a → b and b is a metric_space, is there a definition in mathlib of the pullback metric space structure on a?

[Daniel Roca González]

(That one should definitely not be an instance by default, but it could be a def)

[Daniel Roca González]

Yaël Dillies said:

local attribute [-instance] your_instance

thak you! that's what I wanted

[Reid Barton]

docs#metric_space.induced

[Daniel Roca González]

Turns out nat isn't a metric space either?

[Kevin Buzzard]

Perhaps for the same reason

[Yury G. Kudryashov]

int is a metric space. Note that you should make the metric_space structure compatible with the discrete topological_space structure.

[Yury G. Kudryashov]

(and introduce it near docs#nat.topological_space if this is not done yet)

[Yury G. Kudryashov]

Have a look at the way we define docs#int.metric_space