## Stream: new members

### Topic: Non-type theorems

#### Bjørn Kjos-Hanssen (Nov 30 2020 at 01:24):

I have a result of this form: M(x) is a metric space iff x<1. Here x is some parameter that the space depends on.

I have proved using instance that, under the assumption x<1, I have a metric_space but is there a natural way to prove that something is not a metric space?

Of course, I can just prove that the relevant axiom fails, e.g., triangle inequality, but I wonder if I can then conclude "it's not (or cannot be made into) a metric space"?

#### Bryan Gin-ge Chen (Nov 30 2020 at 01:32):

\not metric_space X is short for metric_space X -> false, i.e. that an instance of metric_space X leads to a contradiction.

#### Reid Barton (Nov 30 2020 at 01:55):

It's not very convenient to state this because of how the data and properties of a metric space are bundled together, but you can write something like "there does not exist a metric_space whose distance function equals (blah)".

#### Reid Barton (Nov 30 2020 at 01:55):

If you're just going to prove that the triangle inequality fails directly then it's probably more sensible to just state that instead.

#### Kevin Buzzard (Nov 30 2020 at 02:05):

Note that any type can be made into a metric space by just giving it the discrete metric, so metric_space X -> false is probably not what you want.

#### Bjørn Kjos-Hanssen (Nov 30 2020 at 02:14):

@Kevin Buzzard yeah, I didn't mean it literally :upside_down:
@Reid Barton that's exactly what I mean, "there does not exist a metric_space with distance function (blah)". Imagine that for some values of x the triangle inequality fails, for other values the symmetry condition fails...

Last updated: May 14 2021 at 13:24 UTC